def Relation.proj1 {α : Type u_1} {β : Type u_2} (r : Relation α β) : ↥r → ↥r.domain

Equations

• r.proj1 ⟨(a, snd), h⟩ = ⟨a, ⋯⟩

def Relation.proj2 {α : Type u_1} {β : Type u_2} (r : Relation α β) : ↥r → ↥r.range

Equations

• r.proj2 ⟨(a, snd), h⟩ = ⟨snd, ⋯⟩

@[simp]

theorem Relation.proj1_val {α : Type u_1} {β : Type u_2} {r : Relation α β} {a : ↥r} : (r.proj1 a).val = a.val.fst

@[simp]

theorem Relation.proj2_val {α : Type u_1} {β : Type u_2} {r : Relation α β} {a : ↥r} : (r.proj2 a).val = a.val.snd

@[simp]

theorem Relation.proj1_val' {α : Type u_1} {β : Type u_2} {r : Relation α β} {a : α} {b : β} {h : (a, b) ∈ r} : (r.proj1 ⟨(a, b), h⟩).val = a

@[simp]

theorem Relation.proj2_val' {α : Type u_1} {β : Type u_2} {r : Relation α β} {a : α} {b : β} {h : (a, b) ∈ r} : (r.proj2 ⟨(a, b), h⟩).val = b

theorem Relation.proj1_surj {α : Type u_1} {β : Type u_2} {r : Relation α β} : Function.Surjective r.proj1

theorem Relation.proj2_surj {α : Type u_1} {β : Type u_2} {r : Relation α β} : Function.Surjective r.proj2

def Relation.proj1_inj_domain_iff_functional {α : Type u_1} {β : Type u_2} {r : Relation α β} : Function.Injective r.proj1 ∧ r.domain = Set.univ ↔ r.Functional

Equations

• ⋯ = ⋯