Theorems · Definition · logic and foundations

Relation.Map

{α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → {δ : Type u_4} → (α → β → Prop) → (α → γ) → (β → δ) → γ → δ → Prop

The map of a relation r through a pair of functions pushes the relation to the codomains of the functions. The resulting relation is defined by having pairs of terms related if they have preimages related by r.

Defined in

Mathlib.Logic.Relation

Cited by

40 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms