Relations as sets of pairs

This file provides API to regard relations between α and β as sets of pairs Set (α × β).

This is in particular useful in the study of uniform spaces, which are topological spaces equipped with a uniformity, namely a filter of pairs α × α whose elements can be viewed as "proximity" relations.

Main declarations

• Rel α β: Type of relations between α and β.
• Rel.inv: Turn R : Rel α β into R.inv : Rel β α by swapping the arguments.
• Rel.dom: Domain of a relation. a ∈ R.dom iff there exists b such that a ~[R] b.
• Rel.cod: Codomain of a relation. b ∈ R.cod iff there exists a such that a ~[R] b.
• Rel.id: The identity relation Rel α α.
• Rel.comp: Relation composition. Note that the arguments order follows the category theory convention, namely (R ○ S) a c ↔ ∃ b, a ~[R] b ∧ b ~[S] z.
• Rel.image: Image of a set under a relation. b ∈ image R s iff there exists a ∈ s such that a ~[R] b. If R is the graph of f (a ~[R] b ↔ f a = b), then R.image = Set.image f.
• Rel.preimage: Preimage of a set under a relation. a ∈ preimage R t iff there exists b ∈ t such that a ~[R] b. If R is the graph of f (a ~[R] b ↔ f a = b), then R.preimage = Set.preimage f.
• Rel.core: Core of a set. For t : Set β, a ∈ R.core t iff all b related to a are in t.
• Rel.restrictDomain: Domain-restriction of a relation to a subtype.
• Function.graph: Graph of a function as a relation.

Implementation notes

There is tension throughout the library between considering relations between α and β simply as α → β → Prop, or as a bundled object Rel α β with dedicated operations and API.

The former approach is used almost everywhere as it is very lightweight and has arguably native support from core Lean features, but it cracks at the seams whenever one starts talking about operations on relations. For example:

• composition of relations R : α → β → Prop, S : β → γ → Prop is Relation.Comp R S := fun a c ↦ ∃ b, R a b ∧ S b c
• map of a relation R : α → β → Prop under f : α → γ, g : β → δ is Relation.map R f g := fun c d ↦ ∃ a b, r a b ∧ f a = c ∧ g b = d.

The latter approach is embodied by Rel α β, with dedicated notation like ○ for composition.

Previously, Rel suffered from the leakage of its definition as

def Rel (α β : Type*) := α → β → Prop

The fact that Rel wasn't an abbrev confuses automation. But simply making it an abbrev would have killed the point of having a separate less see-through type to perform relation operations on, so we instead redefined

def Rel (α β : Type*) := Set (α × β) → Prop

This extra level of indirection guides automation correctly and prevents (some kinds of) leakage.

Simultaneously, uniform spaces need a theory of relations on a type α as elements of Set (α × α), and the new definition of Rel fulfills this role quite well.

@[reducible, inline]

abbrev Rel (α : Type u_5) (β : Type u_6) : Type (max u_6 u_5)

A relation on α and β, aka a set-valued function, aka a partial multifunction.

We represent them as sets due to how relations are used in the context of uniform spaces.

Equations

• Rel α β = Set (α × β)

def Rel.«term_~[_]_» : Lean.TrailingParserDescr

Notation for apply a relation R : Rel α β to a : α, b : β, scoped to the Rel namespace.

Since Rel α β := Set (α × β), a ~[R] b is simply notation for (a, b) ∈ R, but this should be considered an implementation detail.

Equations

• One or more equations did not get rendered due to their size.

def Rel.inv {α : Type u_1} {β : Type u_2} (R : Rel α β) : Rel β α

The inverse relation : R.inv x y ↔ R y x. Note that this is not a groupoid inverse.

Equations

• R.inv = Prod.swap ⁻¹' R

@[simp]

theorem Rel.mem_inv {α : Type u_1} {β : Type u_2} {R : Rel α β} {a : α} {b : β} : (b, a) ∈ R.inv ↔ (a, b) ∈ R

@[deprecated Rel.mem_inv (since := "2025-07-06")]

theorem Rel.inv_def {α : Type u_1} {β : Type u_2} {R : Rel α β} {a : α} {b : β} : (b, a) ∈ R.inv ↔ (a, b) ∈ R

Alias of Rel.mem_inv.

@[simp]

theorem Rel.inv_inv {α : Type u_1} {β : Type u_2} {R : Rel α β} : R.inv.inv = R

theorem Rel.inv_mono {α : Type u_1} {β : Type u_2} {r₁ r₂ : Rel α β} (h : r₁ ⊆ r₂) : r₁.inv ⊆ r₂.inv

@[simp]

theorem Rel.inv_empty {α : Type u_1} {β : Type u_2} : ∅.inv = ∅

@[simp]

theorem Rel.inv_univ {α : Type u_1} {β : Type u_2} : inv Set.univ = Set.univ

@[deprecated Rel.inv_empty (since := "2025-07-06")]

theorem Rel.inv_bot {α : Type u_1} {β : Type u_2} : ∅.inv = ∅

Alias of Rel.inv_empty.

def Rel.dom {α : Type u_1} {β : Type u_2} (R : Rel α β) : Set α

Domain of a relation.

Equations

• R.dom = {a : α | ∃ (b : β), (a, b) ∈ R}

def Rel.cod {α : Type u_1} {β : Type u_2} (R : Rel α β) : Set β

Codomain of a relation, aka range.

Equations

• R.cod = {b : β | ∃ (a : α), (a, b) ∈ R}

@[deprecated Rel.cod (since := "2025-07-06")]

def Rel.codom {α : Type u_1} {β : Type u_2} (R : Rel α β) : Set β

Alias of Rel.cod.

---

Codomain of a relation, aka range.

Equations

• @Rel.codom = @Rel.cod

@[simp]

theorem Rel.mem_dom {α : Type u_1} {β : Type u_2} {R : Rel α β} {a : α} : a ∈ R.dom ↔ ∃ (b : β), (a, b) ∈ R

@[simp]

theorem Rel.mem_cod {α : Type u_1} {β : Type u_2} {R : Rel α β} {b : β} : b ∈ R.cod ↔ ∃ (a : α), (a, b) ∈ R

theorem Rel.dom_mono {α : Type u_1} {β : Type u_2} {r₁ r₂ : Rel α β} (h : r₁ ≤ r₂) : r₁.dom ⊆ r₂.dom

theorem Rel.cod_mono {α : Type u_1} {β : Type u_2} {r₁ r₂ : Rel α β} (h : r₁ ≤ r₂) : r₁.cod ⊆ r₂.cod

@[simp]

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

@[simp]

theorem Rel.cod_empty {α : Type u_1} {β : Type u_2} : ∅.cod = ∅

@[simp]

theorem Rel.dom_univ {α : Type u_1} {β : Type u_2} [Nonempty β] : dom Set.univ = Set.univ

@[simp]

theorem Rel.cod_univ {α : Type u_1} {β : Type u_2} [Nonempty α] : cod Set.univ = Set.univ

@[simp]

theorem Rel.cod_inv {α : Type u_1} {β : Type u_2} {R : Rel α β} : R.inv.cod = R.dom

@[simp]

theorem Rel.dom_inv {α : Type u_1} {β : Type u_2} {R : Rel α β} : R.inv.dom = R.cod

@[deprecated Rel.cod_inv (since := "2025-07-06")]

theorem Rel.codom_inv {α : Type u_1} {β : Type u_2} {R : Rel α β} : R.inv.cod = R.dom

Alias of Rel.cod_inv.

def Rel.id {α : Type u_1} : Rel α α

The identity relation.

Equations

• Rel.id = {(a₁, a₂) : α × α | a₁ = a₂}

@[simp]

theorem Rel.mem_id {α : Type u_1} {a₁ a₂ : α} : (a₁, a₂) ∈ Rel.id ↔ a₁ = a₂

@[simp]

theorem Rel.inv_id {α : Type u_1} : Rel.id.inv = Rel.id

def Rel.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : Rel α β) (S : Rel β γ) : Rel α γ

Composition of relation.

Note that this follows the CategoryTheory order of arguments.

Equations

• R.comp S = {(a, c) : α × γ | ∃ (b : β), (a, b) ∈ R ∧ (b, c) ∈ S}

def Rel.«term_○_» : Lean.TrailingParserDescr

Composition of relation.

Note that this follows the CategoryTheory order of arguments.

Equations

• Rel.«term_○_» = Lean.ParserDescr.trailingNode `Rel.«term_○_» 62 62 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ○ ") (Lean.ParserDescr.cat `term 63))

@[simp]

theorem Rel.mem_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : Rel α β} {S : Rel β γ} {a : α} {c : γ} : (a, c) ∈ R.comp S ↔ ∃ (b : β), (a, b) ∈ R ∧ (b, c) ∈ S

theorem Rel.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (R : Rel α β) (S : Rel β γ) (t : Rel γ δ) : (R.comp S).comp t = R.comp (S.comp t)

@[simp]

theorem Rel.comp_id {α : Type u_1} {β : Type u_2} (R : Rel α β) : R.comp Rel.id = R

@[simp]

theorem Rel.id_comp {α : Type u_1} {β : Type u_2} (R : Rel α β) : Rel.id.comp R = R

@[simp]

theorem Rel.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : Rel α β) (S : Rel β γ) : (R.comp S).inv = S.inv.comp R.inv

@[simp]

theorem Rel.comp_empty {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : Rel α β) : R.comp ∅ = ∅

@[simp]

theorem Rel.empty_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (S : Rel β γ) : ∅.comp S = ∅

@[simp]

theorem Rel.comp_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : Rel α β) : R.comp Set.univ = {(a, _c) : α × γ | a ∈ R.dom}

@[simp]

theorem Rel.univ_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (S : Rel β γ) : comp Set.univ S = {(_b, c) : α × γ | c ∈ S.cod}

@[deprecated Rel.comp_univ (since := "2025-07-06")]

theorem Rel.comp_right_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : Rel α β) : R.comp Set.univ = {(a, _c) : α × γ | a ∈ R.dom}

Alias of Rel.comp_univ.

@[deprecated Rel.univ_comp (since := "2025-07-06")]

theorem Rel.comp_left_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} (S : Rel β γ) : comp Set.univ S = {(_b, c) : α × γ | c ∈ S.cod}

Alias of Rel.univ_comp.

def Rel.image {α : Type u_1} {β : Type u_2} (R : Rel α β) (s : Set α) : Set β

Image of a set under a relation.

Equations

• R.image s = {b : β | ∃ a ∈ s, (a, b) ∈ R}

def Rel.preimage {α : Type u_1} {β : Type u_2} (R : Rel α β) (t : Set β) : Set α

Preimage of a set t under a relation R. Same as the image of t under R.inv.

Equations

• R.preimage t = {a : α | ∃ b ∈ t, (a, b) ∈ R}

@[simp]

theorem Rel.mem_image {α : Type u_1} {β : Type u_2} {R : Rel α β} {s : Set α} {b : β} : b ∈ R.image s ↔ ∃ a ∈ s, (a, b) ∈ R

@[simp]

theorem Rel.mem_preimage {α : Type u_1} {β : Type u_2} {R : Rel α β} {t : Set β} {a : α} : a ∈ R.preimage t ↔ ∃ b ∈ t, (a, b) ∈ R

theorem Rel.image_subset_image {α : Type u_1} {β : Type u_2} {R : Rel α β} {s₁ s₂ : Set α} (hs : s₁ ⊆ s₂) : R.image s₁ ⊆ R.image s₂

theorem Rel.preimage_subset_preimage {α : Type u_1} {β : Type u_2} {R : Rel α β} {t₁ t₂ : Set β} (ht : t₁ ⊆ t₂) : R.preimage t₁ ⊆ R.preimage t₂

@[simp]

theorem Rel.image_inv {α : Type u_1} {β : Type u_2} (R : Rel α β) (t : Set β) : R.inv.image t = R.preimage t

@[simp]

theorem Rel.preimage_inv {α : Type u_1} {β : Type u_2} (R : Rel α β) (s : Set α) : R.inv.preimage s = R.image s

theorem Rel.image_mono {α : Type u_1} {β : Type u_2} {R : Rel α β} : Monotone R.image

theorem Rel.preimage_mono {α : Type u_1} {β : Type u_2} {R : Rel α β} : Monotone R.preimage

@[simp]

theorem Rel.image_empty_right {α : Type u_1} {β : Type u_2} {R : Rel α β} : R.image ∅ = ∅

@[simp]

theorem Rel.preimage_empty_right {α : Type u_1} {β : Type u_2} {R : Rel α β} : R.preimage ∅ = ∅

@[simp]

theorem Rel.image_univ_right {α : Type u_1} {β : Type u_2} {R : Rel α β} : R.image Set.univ = R.cod

@[simp]

theorem Rel.preimage_univ_right {α : Type u_1} {β : Type u_2} {R : Rel α β} : R.preimage Set.univ = R.dom

theorem Rel.image_inter_subset {α : Type u_1} {β : Type u_2} (R : Rel α β) {s₁ s₂ : Set α} : R.image (s₁ ∩ s₂) ⊆ R.image s₁ ∩ R.image s₂

@[deprecated Rel.image_inter_subset (since := "2025-07-06")]

theorem Rel.preimage_top {α : Type u_1} {β : Type u_2} (R : Rel α β) {s₁ s₂ : Set α} : R.image (s₁ ∩ s₂) ⊆ R.image s₁ ∩ R.image s₂

Alias of Rel.image_inter_subset.

theorem Rel.preimage_inter_subset {α : Type u_1} {β : Type u_2} (R : Rel α β) {t₁ t₂ : Set β} : R.preimage (t₁ ∩ t₂) ⊆ R.preimage t₁ ∩ R.preimage t₂

@[deprecated Rel.preimage_inter_subset (since := "2025-07-06")]

theorem Rel.image_eq_dom_of_codomain_subset {α : Type u_1} {β : Type u_2} (R : Rel α β) {t₁ t₂ : Set β} : R.preimage (t₁ ∩ t₂) ⊆ R.preimage t₁ ∩ R.preimage t₂

Alias of Rel.preimage_inter_subset.

theorem Rel.image_union {α : Type u_1} {β : Type u_2} (R : Rel α β) (s₁ s₂ : Set α) : R.image (s₁ ∪ s₂) = R.image s₁ ∪ R.image s₂

@[deprecated Rel.image_union (since := "2025-07-06")]

theorem Rel.preimage_eq_codom_of_domain_subset {α : Type u_1} {β : Type u_2} (R : Rel α β) (s₁ s₂ : Set α) : R.image (s₁ ∪ s₂) = R.image s₁ ∪ R.image s₂

Alias of Rel.image_union.

theorem Rel.preimage_union {α : Type u_1} {β : Type u_2} (R : Rel α β) (t₁ t₂ : Set β) : R.preimage (t₁ ∪ t₂) = R.preimage t₁ ∪ R.preimage t₂

@[simp]

theorem Rel.image_id {α : Type u_1} (s : Set α) : Rel.id.image s = s

@[simp]

theorem Rel.preimage_id {α : Type u_1} (s : Set α) : Rel.id.preimage s = s

theorem Rel.image_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : Rel α β) (S : Rel β γ) (s : Set α) : (R.comp S).image s = S.image (R.image s)

theorem Rel.preimage_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : Rel α β) (S : Rel β γ) (u : Set γ) : (R.comp S).preimage u = R.preimage (S.preimage u)

@[simp]

theorem Rel.image_empty_left {α : Type u_1} {β : Type u_2} (s : Set α) : ∅.image s = ∅

@[simp]

theorem Rel.preimage_empty_left {α : Type u_1} {β : Type u_2} (t : Set β) : ∅.preimage t = ∅

@[deprecated Rel.preimage_empty_left (since := "2025-07-06")]

theorem Rel.preimage_bot {α : Type u_1} {β : Type u_2} (t : Set β) : ∅.preimage t = ∅

Alias of Rel.preimage_empty_left.

@[simp]

theorem Rel.image_univ_left {α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Nonempty) : image Set.univ s = Set.univ

@[simp]

theorem Rel.preimage_univ_left {α : Type u_1} {β : Type u_2} {t : Set β} (ht : t.Nonempty) : preimage Set.univ t = Set.univ

theorem Rel.image_eq_cod_of_dom_subset {α : Type u_1} {β : Type u_2} {R : Rel α β} {t : Set β} (h : R.cod ⊆ t) : R.preimage t = R.dom

theorem Rel.preimage_eq_dom_of_cod_subset {α : Type u_1} {β : Type u_2} {R : Rel α β} {t : Set β} (h : R.cod ⊆ t) : R.preimage t = R.dom

@[simp]

theorem Rel.image_inter_dom {α : Type u_1} {β : Type u_2} (R : Rel α β) (s : Set α) : R.image (s ∩ R.dom) = R.image s

@[simp]

theorem Rel.preimage_inter_cod {α : Type u_1} {β : Type u_2} (R : Rel α β) (t : Set β) : R.preimage (t ∩ R.cod) = R.preimage t

@[deprecated Rel.preimage_inter_cod (since := "2025-07-06")]

theorem Rel.preimage_inter_codom_eq {α : Type u_1} {β : Type u_2} (R : Rel α β) (t : Set β) : R.preimage (t ∩ R.cod) = R.preimage t

Alias of Rel.preimage_inter_cod.

theorem Rel.inter_dom_subset_preimage_image {α : Type u_1} {β : Type u_2} {R : Rel α β} {s : Set α} : s ∩ R.dom ⊆ R.preimage (R.image s)

theorem Rel.inter_cod_subset_image_preimage {α : Type u_1} {β : Type u_2} {R : Rel α β} {t : Set β} : t ∩ R.cod ⊆ R.image (R.preimage t)

@[deprecated Rel.inter_cod_subset_image_preimage (since := "2025-07-06")]

theorem Rel.image_preimage_subset_inter_codom {α : Type u_1} {β : Type u_2} {R : Rel α β} {t : Set β} : t ∩ R.cod ⊆ R.image (R.preimage t)

Alias of Rel.inter_cod_subset_image_preimage.

def Rel.core {α : Type u_1} {β : Type u_2} (R : Rel α β) (t : Set β) : Set α

Core of a set S : Set β w.R.t R : Rel α β is the set of x : α that are related only to elements of S. Other generalization of Function.preimage.

Equations

• R.core t = {a : α | ∀ ⦃b : β⦄, (a, b) ∈ R → b ∈ t}

@[simp]

theorem Rel.mem_core {α : Type u_1} {β : Type u_2} {R : Rel α β} {t : Set β} {a : α} : a ∈ R.core t ↔ ∀ ⦃b : β⦄, (a, b) ∈ R → b ∈ t

theorem Rel.core_subset_core {α : Type u_1} {β : Type u_2} {R : Rel α β} {t₁ t₂ : Set β} (ht : t₁ ⊆ t₂) : R.core t₁ ⊆ R.core t₂

theorem Rel.core_mono {α : Type u_1} {β : Type u_2} {R : Rel α β} : Monotone R.core

theorem Rel.core_inter {α : Type u_1} {β : Type u_2} (R : Rel α β) (t₁ t₂ : Set β) : R.core (t₁ ∩ t₂) = R.core t₁ ∩ R.core t₂

theorem Rel.core_union_subset {α : Type u_1} {β : Type u_2} {R : Rel α β} {t₁ t₂ : Set β} : R.core t₁ ∪ R.core t₂ ⊆ R.core (t₁ ∪ t₂)

@[simp]

theorem Rel.core_univ {α : Type u_1} {β : Type u_2} {R : Rel α β} : R.core Set.univ = Set.univ

@[simp]

theorem Rel.core_id {β : Type u_2} (t : Set β) : Rel.id.core t = t

theorem Rel.core_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : Rel α β) (S : Rel β γ) (u : Set γ) : (R.comp S).core u = R.core (S.core u)

theorem Rel.image_subset_iff {α : Type u_1} {β : Type u_2} {R : Rel α β} {s : Set α} {t : Set β} : R.image s ⊆ t ↔ s ⊆ R.core t

theorem Rel.image_core_gc {α : Type u_1} {β : Type u_2} {R : Rel α β} : GaloisConnection R.image R.core

def Rel.restrictDomain {α : Type u_1} {β : Type u_2} (R : Rel α β) (s : Set α) : Rel (↑s) β

Restrict the domain of a relation to a subtype.

Equations

• R.restrictDomain s = {(a, b) : ↑s × β | (↑a, b) ∈ R}

@[reducible, inline]

abbrev Rel.IsTrans {α : Type u_1} (R : Rel α α) : Prop

A relation R is transitive if a ~[R] b and b ~[R] c together imply a ~[R] c.

Equations

• R.IsTrans = IsTrans α fun (x1 x2 : α) => (x1, x2) ∈ R

theorem Rel.trans {α : Type u_1} (R : Rel α α) {a b c : α} [R.IsTrans] (hab : (a, b) ∈ R) (hbc : (b, c) ∈ R) : (a, c) ∈ R

instance Rel.instIsTransSetOfProdMatch_1PropOfIsTrans {α : Type u_1} {R : α → α → Prop} [IsTrans α R] : Rel.IsTrans {(a, b) : α × α | R a b}

@[reducible, inline]

abbrev Rel.IsIrrefl {α : Type u_1} (R : Rel α α) : Prop

A relation R is irreflexive if ¬ a ~[R] a.

Equations

• R.IsIrrefl = IsIrrefl α fun (x1 x2 : α) => (x1, x2) ∈ R

theorem Rel.irrefl {α : Type u_1} (R : Rel α α) (a : α) [R.IsIrrefl] : (a, a) ∉ R

instance Rel.instIsIrreflSetOfProdMatch_1PropOfIsIrrefl {α : Type u_1} {R : α → α → Prop} [IsIrrefl α R] : Rel.IsIrrefl {(a, b) : α × α | R a b}

@[reducible, inline]

abbrev Rel.IsWellFounded {α : Type u_1} (R : Rel α α) : Prop

A relation R on a type α is well-founded if all elements of α are accessible within R.

Equations

• R.IsWellFounded = WellFounded fun (x1 x2 : α) => (x1, x2) ∈ R

@[reducible, inline]

abbrev Rel.Hom {α : Type u_1} {β : Type u_2} (R : Rel α α) (S : Rel β β) : Type (max u_1 u_2)

A relation homomorphism with respect to a given pair of relations R and S s is a function f : α → β such that a ~[R] b → f a ~[s] f b.

Equations

• R.Hom S = ((fun (x1 x2 : α) => (x1, x2) ∈ R) →r fun (x1 x2 : β) => (x1, x2) ∈ S)

def Function.graph {α : Type u_1} {β : Type u_2} (f : α → β) : Rel α β

The graph of a function as a relation.

Equations

• Function.graph f = {(a, b) : α × β | f a = b}

@[simp]

theorem Function.mem_graph {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {b : β} : (a, b) ∈ graph f ↔ f a = b

@[deprecated Function.mem_graph (since := "2025-07-06")]

theorem Function.graph_def {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {b : β} : (a, b) ∈ graph f ↔ f a = b

Alias of Function.mem_graph.

theorem Function.graph_injective {α : Type u_1} {β : Type u_2} : Injective graph

@[simp]

theorem Function.graph_inj {α : Type u_1} {β : Type u_2} {f g : α → β} : graph f = graph g ↔ f = g

@[simp]

theorem Function.graph_id {α : Type u_1} : graph id = Rel.id

theorem Function.graph_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (g : α → β) : graph (f ∘ g) = (graph g).comp (graph f)

theorem Equiv.graph_inv {α : Type u_1} {β : Type u_2} (f : α ≃ β) : Function.graph ⇑f.symm = (Function.graph ⇑f).inv

theorem Rel.exists_graph_eq_iff {α : Type u_1} {β : Type u_2} (R : Rel α β) : (∃! f : α → β, Function.graph f = R) ↔ ∀ (a : α), ∃! b : β, (a, b) ∈ R

@[deprecated Rel.exists_graph_eq_iff (since := "2025-07-06")]

theorem Relation.is_graph_iff {α : Type u_1} {β : Type u_2} (R : Rel α β) : (∃! f : α → β, Function.graph f = R) ↔ ∀ (a : α), ∃! b : β, (a, b) ∈ R

Alias of Rel.exists_graph_eq_iff.

theorem Set.image_eq {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : f '' s = (Function.graph f).image s

theorem Set.preimage_eq {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β) : f ⁻¹' s = (Function.graph f).preimage s

theorem Set.preimage_eq_core {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β) : f ⁻¹' s = (Function.graph f).core s