Relations: Domain and Codomain

This module proves basic properties of the domain and codomain of relations.

References

• Simple Laws about Nonprominent Properties of Binary Relations

@[simp]

theorem Relation.emptyHRelation_emptyRelation {α : Sort u_1} : emptyHRelation = emptyRelation

@[simp]

theorem Relation.emptyHrelation_apply {α : Sort u_1} {β : Sort u_2} (a : α) (b : β) : emptyHRelation a b ↔ False

@[simp]

theorem Relation.mem_dom {α : Type u_2} {β : Type u_1} {r : α → β → Prop} {a : α} : a ∈ dom r ↔ ∃ (b : β), r a b

@[simp]

theorem Relation.mem_cod {α : Sort u_2} {β : Type u_1} {r : α → β → Prop} {b : β} : b ∈ cod r ↔ ∃ (a : α), r a b

theorem Relation.dom_mono {ι✝ : Type u_2} {ι✝¹ : Type u_3} {r₁ r₂ : ι✝ → ι✝¹ → Prop} (h : r₁ ≤ r₂) : dom r₁ ⊆ dom r₂

theorem Relation.cod_mono {ι✝ : Type u_2} {ι✝¹ : Type u_3} {r₁ r₂ : ι✝ → ι✝¹ → Prop} (h : r₁ ≤ r₂) : cod r₁ ⊆ cod r₂

@[simp]

theorem Relation.dom_empty {α : Type u_2} {β : Type u_1} : dom emptyHRelation = ∅

@[simp]

theorem Relation.cod_empty {α : Sort u_2} {β : Type u_1} : cod emptyHRelation = ∅

@[simp]

theorem Relation.dom_eq_empty_iff {α : Type u_2} {β : Type u_1} {r : α → β → Prop} : dom r = ∅ ↔ r = emptyHRelation

@[simp]

theorem Relation.cod_eq_empty_iff {α : Sort u_2} {β : Type u_1} {r : α → β → Prop} : cod r = ∅ ↔ r = emptyHRelation

@[simp]

theorem Relation.cod_inv {α : Type u_2} {β : Type u_1} {r : α → β → Prop} : (cod fun (a : β) (b : α) => r b a) = dom r

@[simp]

theorem Relation.dom_inv {α : Sort u_2} {β : Type u_1} {r : α → β → Prop} : (dom fun (a : β) (b : α) => r b a) = cod r

theorem Std.Trichotomous.subsingleton_cod {α : Type u_2} (r : α → α → Prop) [Trichotomous r] : Subsingleton ↑(Relation.cod r)ᶜ

theorem Std.Trichotomous.subsingleton_dom {α : Type u_2} (r : α → α → Prop) [Trichotomous r] : Subsingleton ↑(Relation.dom r)ᶜ