theorem Relation.functional_iff_disjoint_preimage_disjoint {α : Type u_1} {β : Type u_2} {r : Relation α β} : r.Functional ↔ r.domain = Set.univ ∧ ∀ (x y : Set β), x ∩ y = ∅ → r.preimage x ∩ r.preimage y = ∅

theorem Relation.image_eq_range_inter {α : Type u_1} {β : Type u_2} {r : Relation α β} {x : Set α} : r.image x = (r ∩ x.prod r.range).range

theorem Relation.image_eq_image_inter_domain {α : Type u_1} {β : Type u_2} {r : Relation α β} {x : Set α} : r.image x = r.image (x ∩ r.domain)