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

• SetRel α β: Type of relations between α and β.
• SetRel.inv: Turn R : SetRel α β into R.inv : SetRel β α by swapping the arguments.
• SetRel.dom: Domain of a relation. a ∈ R.dom iff there exists b such that a ~[R] b.
• SetRel.cod: Codomain of a relation. b ∈ R.cod iff there exists a such that a ~[R] b.
• SetRel.id: The identity relation SetRel α α.
• SetRel.comp: SetRelation composition. Note that the arguments order follows the category theory convention, namely (R ○ S) a c ↔ ∃ b, a ~[R] b ∧ b ~[S] z.
• SetRel.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.
• SetRel.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.
• SetRel.core: Core of a set. For t : Set β, a ∈ R.core t iff all b related to a are in t.
• SetRel.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 SetRel α β 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 SetRelation.Comp R S := fun a c ↦ ∃ b, R a b ∧ S b c
• map of a relation R : α → β → Prop under f : α → γ, g : β → δ is SetRelation.map R f g := fun c d ↦ ∃ a b, r a b ∧ f a = c ∧ g b = d.

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

Previously, SetRel suffered from the leakage of its definition as

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

The fact that SetRel 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 SetRel (α β : 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 SetRel fulfills this role quite well.

@[reducible, inline]

abbrev SetRel (α : Type u_6) (β : Type u_7) : Type (max u_7 u_6)

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

• SetRel α β = Set (α × β)

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

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

Since SetRel α β := 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 SetRel.inv {α : Type u_1} {β : Type u_2} (R : SetRel α β) : SetRel β α

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 SetRel.mem_inv {α : Type u_1} {β : Type u_2} {R : SetRel α β} {a : α} {b : β} : (b, a) ∈ R.inv ↔ (a, b) ∈ R

@[simp]

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

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

@[simp]

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

@[simp]

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

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

Domain of a relation.

Equations

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

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

Codomain of a relation, aka range.

Equations

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem SetRel.dom_eq_empty_iff {α : Type u_1} {β : Type u_2} {R : SetRel α β} : R.dom = ∅ ↔ R = ∅

@[simp]

theorem SetRel.cod_eq_empty_iff {α : Type u_1} {β : Type u_2} {R : SetRel α β} : R.cod = ∅ ↔ R = ∅

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The identity relation.

Equations

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

@[simp]

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

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

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

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 SetRel.«term_○_» : Lean.TrailingParserDescr

Composition of relation.

Note that this follows the CategoryTheory order of arguments.

Equations

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

@[simp]

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

theorem SetRel.prodMk_mem_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : SetRel α β} {S : SetRel β γ} {a : α} {b : β} {c : γ} (hab : (a, b) ∈ R) (hbc : (b, c) ∈ S) : (a, c) ∈ R.comp S

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem SetRel.comp_iUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (R : SetRel α β) (S : ι → SetRel β γ) : R.comp (⋃ (i : ι), S i) = ⋃ (i : ι), R.comp (S i)

theorem SetRel.iUnion_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (R : ι → SetRel α β) (S : SetRel β γ) : comp (⋃ (i : ι), R i) S = ⋃ (i : ι), (R i).comp S

theorem SetRel.comp_sUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (𝒮 : Set (SetRel β γ)) : R.comp (⋃₀ 𝒮) = ⋃ S ∈ 𝒮, R.comp S

theorem SetRel.sUnion_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (ℛ : Set (SetRel α β)) (S : SetRel β γ) : comp (⋃₀ ℛ) S = ⋃ R ∈ ℛ, R.comp S

theorem SetRel.comp_subset_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R₁ R₂ : SetRel α β} {S₁ S₂ : SetRel β γ} (hR : R₁ ⊆ R₂) (hS : S₁ ⊆ S₂) : R₁.comp S₁ ⊆ R₂.comp S₂

theorem SetRel.comp_subset_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R₁ R₂ : SetRel α β} {S : SetRel β γ} (hR : R₁ ⊆ R₂) : R₁.comp S ⊆ R₂.comp S

theorem SetRel.comp_subset_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : SetRel α β} {S₁ S₂ : SetRel β γ} (hS : S₁ ⊆ S₂) : R.comp S₁ ⊆ R.comp S₂

theorem Monotone.relComp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_6} [Preorder ι] {f : ι → SetRel α β} {g : ι → SetRel β γ} (hf : Monotone f) (hg : Monotone g) : Monotone fun (x : ι) => (f x).comp (g x)

theorem SetRel.prod_comp_prod_of_inter_nonempty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t₁ t₂ : Set β} (ht : (t₁ ∩ t₂).Nonempty) (s : Set α) (u : Set γ) : comp (s ×ˢ t₁) (t₂ ×ˢ u) = s ×ˢ u

theorem SetRel.prod_comp_prod_of_disjoint {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t₁ t₂ : Set β} (ht : Disjoint t₁ t₂) (s : Set α) (u : Set γ) : comp (s ×ˢ t₁) (t₂ ×ˢ u) = ∅

theorem SetRel.prod_comp_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set α) (t₁ t₂ : Set β) (u : Set γ) [Decidable (Disjoint t₁ t₂)] : comp (s ×ˢ t₁) (t₂ ×ˢ u) = if Disjoint t₁ t₂ then ∅ else s ×ˢ u

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

Image of a set under a relation.

Equations

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

def SetRel.preimage {α : Type u_1} {β : Type u_2} (R : SetRel α β) (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 : β), b ∈ t ∧ (a, b) ∈ R}

@[simp]

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

@[simp]

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

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

theorem SetRel.image_subset_image_left {α : Type u_1} {β : Type u_2} {R₁ R₂ : SetRel α β} {s : Set α} (hR : R₁ ⊆ R₂) : R₁.image s ⊆ R₂.image s

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

theorem SetRel.preimage_subset_preimage_left {α : Type u_1} {β : Type u_2} {R₁ R₂ : SetRel α β} {t : Set β} (hR : R₁ ⊆ R₂) : R₁.preimage t ⊆ R₂.preimage t

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

theorem SetRel.image_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_5} (R : SetRel α β) (s : ι → Set α) : R.image (⋃ (i : ι), s i) = ⋃ (i : ι), R.image (s i)

theorem SetRel.image_sUnion {α : Type u_1} {β : Type u_2} (R : SetRel α β) (S : Set (Set α)) : R.image (⋃₀ S) = ⋃ s ∈ S, R.image s

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

theorem SetRel.preimage_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_5} (R : SetRel α β) (t : ι → Set β) : R.preimage (⋃ (i : ι), t i) = ⋃ (i : ι), R.preimage (t i)

theorem SetRel.preimage_sUnion {α : Type u_1} {β : Type u_2} (R : SetRel α β) (T : Set (Set β)) : R.preimage (⋃₀ T) = ⋃ t ∈ T, R.preimage t

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

theorem SetRel.image_eq_biUnion {α : Type u_1} {β : Type u_2} {R : SetRel α β} {s : Set α} : R.image s = ⋃ x ∈ s, {y : β | (x, y) ∈ R}

theorem SetRel.preimage_eq_biUnion {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β} : R.preimage t = ⋃ y ∈ t, {x : α | (x, y) ∈ R}

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

Core of a set S : Set β w.R.t R : SetRel α β 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 SetRel.mem_core {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β} {a : α} : a ∈ R.core t ↔ ∀ ⦃b : β⦄, (a, b) ∈ R → b ∈ t

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

Restrict the domain of a relation to a subtype.

Equations

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

Reflexive relations

@[reducible, inline]

abbrev SetRel.IsRefl {α : Type u_1} (R : SetRel α α) : Prop

A relation R is reflexive if a ~[R] a.

Equations

• R.IsRefl = Std.Refl fun (x1 x2 : α) => (x1, x2) ∈ R

theorem SetRel.refl {α : Type u_1} (R : SetRel α α) [R.IsRefl] (a : α) : (a, a) ∈ R

theorem SetRel.rfl {α : Type u_1} (R : SetRel α α) {a : α} [R.IsRefl] : (a, a) ∈ R

theorem SetRel.id_subset {α : Type u_1} {R : SetRel α α} [R.IsRefl] : SetRel.id ⊆ R

theorem SetRel.id_subset_iff {α : Type u_1} {R : SetRel α α} : SetRel.id ⊆ R ↔ R.IsRefl

instance SetRel.isRefl_univ {α : Type u_1} : SetRel.IsRefl Set.univ

instance SetRel.isRefl_inter {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsRefl] [R₂.IsRefl] : (R₁ ∩ R₂).IsRefl

instance SetRel.IsRefl.comp {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsRefl] [R₂.IsRefl] : (R₁.comp R₂).IsRefl

theorem SetRel.IsRefl.sInter {α : Type u_1} {ℛ : Set (SetRel α α)} (hℛ : ∀ (R : SetRel α α), R ∈ ℛ → R.IsRefl) : SetRel.IsRefl (⋂₀ ℛ)

instance SetRel.isRefl_iInter {α : Type u_1} {ι : Sort u_5} {R : ι → SetRel α α} [∀ (i : ι), (R i).IsRefl] : SetRel.IsRefl (⋂ (i : ι), R i)

instance SetRel.isRefl_preimage {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : β → α} [R.IsRefl] : SetRel.IsRefl (Prod.map f f ⁻¹' R)

theorem SetRel.isRefl_mono {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsRefl] (hR : R₁ ⊆ R₂) : R₂.IsRefl

theorem SetRel.left_subset_comp {α : Type u_1} {β : Type u_2} {S : SetRel β β} {R : SetRel α β} [S.IsRefl] : R ⊆ R.comp S

theorem SetRel.right_subset_comp {α : Type u_1} {β : Type u_2} {R : SetRel α α} [R.IsRefl] {S : SetRel α β} : S ⊆ R.comp S

theorem SetRel.subset_iterate_comp {α : Type u_1} {β : Type u_2} {R : SetRel α α} [R.IsRefl] {S : SetRel α β} {n : ℕ} : S ⊆ (fun (x : SetRel α β) => R.comp x)^[n] S

theorem SetRel.self_subset_image {α : Type u_1} {R : SetRel α α} [R.IsRefl] (s : Set α) : s ⊆ R.image s

theorem SetRel.self_subset_preimage {α : Type u_1} {R : SetRel α α} [R.IsRefl] (s : Set α) : s ⊆ R.preimage s

theorem SetRel.exists_eq_singleton_of_prod_subset_id {α : Type u_1} {s t : Set α} (hs : s.Nonempty) (ht : t.Nonempty) (hst : s ×ˢ t ⊆ SetRel.id) : ∃ (x : α), s = {x} ∧ t = {x}

Symmetric relations

@[reducible, inline]

abbrev SetRel.IsSymm {α : Type u_1} (R : SetRel α α) : Prop

A relation R is symmetric if a ~[R] b ↔ b ~[R] a.

Equations

• R.IsSymm = Std.Symm fun (x1 x2 : α) => (x1, x2) ∈ R

theorem SetRel.symm {α : Type u_1} (R : SetRel α α) {a b : α} [R.IsSymm] (hab : (a, b) ∈ R) : (b, a) ∈ R

theorem SetRel.comm {α : Type u_1} (R : SetRel α α) {a b : α} [R.IsSymm] : (a, b) ∈ R ↔ (b, a) ∈ R

@[simp]

theorem SetRel.inv_eq_self {α : Type u_1} (R : SetRel α α) [R.IsSymm] : R.inv = R

theorem SetRel.inv_eq_self_iff {α : Type u_1} {R : SetRel α α} : R.inv = R ↔ R.IsSymm

instance SetRel.instIsSymmInv {α : Type u_1} {R : SetRel α α} [R.IsSymm] : R.inv.IsSymm

instance SetRel.isSymm_empty {α : Type u_1} : ∅.IsSymm

instance SetRel.isSymm_univ {α : Type u_1} : SetRel.IsSymm Set.univ

instance SetRel.isSymm_inter {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsSymm] [R₂.IsSymm] : (R₁ ∩ R₂).IsSymm

theorem SetRel.IsSymm.sInter {α : Type u_1} {ℛ : Set (SetRel α α)} (hℛ : ∀ (R : SetRel α α), R ∈ ℛ → R.IsSymm) : SetRel.IsSymm (⋂₀ ℛ)

instance SetRel.isSymm_iInter {α : Type u_1} {ι : Sort u_5} {R : ι → SetRel α α} [∀ (i : ι), (R i).IsSymm] : SetRel.IsSymm (⋂ (i : ι), R i)

instance SetRel.isSymm_id {α : Type u_1} : SetRel.id.IsSymm

instance SetRel.isSymm_preimage {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : β → α} [R.IsSymm] : SetRel.IsSymm (Prod.map f f ⁻¹' R)

instance SetRel.isSymm_image {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : α → β} [R.IsSymm] : SetRel.IsSymm (Prod.map f f '' R)

instance SetRel.isSymm_comp_inv {α : Type u_1} {R : SetRel α α} : (R.comp R.inv).IsSymm

instance SetRel.isSymm_inv_comp {α : Type u_1} {R : SetRel α α} : (R.inv.comp R).IsSymm

instance SetRel.isSymm_comp_self {α : Type u_1} {R : SetRel α α} [R.IsSymm] : (R.comp R).IsSymm

theorem SetRel.prod_subset_comm {α : Type u_1} {s₁ s₂ : Set α} {R : SetRel α α} [R.IsSymm] : s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R

def SetRel.symmetrize {α : Type u_1} (R : SetRel α α) : SetRel α α

The maximal symmetric relation contained in a given relation.

Equations

• R.symmetrize = R ∩ R.inv

instance SetRel.isSymm_symmetrize {α : Type u_1} {R : SetRel α α} : R.symmetrize.IsSymm

theorem SetRel.symmetrize_subset_self {α : Type u_1} {R : SetRel α α} : R.symmetrize ⊆ R

theorem SetRel.symmetrize_subset_inv {α : Type u_1} {R : SetRel α α} : R.symmetrize ⊆ R.inv

theorem SetRel.subset_symmetrize {α : Type u_1} {R S : SetRel α α} : S ⊆ R.symmetrize ↔ S ⊆ R ∧ S ⊆ R.inv

theorem SetRel.symmetrize_mono {α : Type u_1} {R₁ R₂ : SetRel α α} (h : R₁ ⊆ R₂) : R₁.symmetrize ⊆ R₂.symmetrize

Transitive relations

@[reducible, inline]

abbrev SetRel.IsTrans {α : Type u_1} (R : SetRel α α) : 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 SetRel.trans {α : Type u_1} (R : SetRel α α) {a b c : α} [R.IsTrans] (hab : (a, b) ∈ R) (hbc : (b, c) ∈ R) : (a, c) ∈ R

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

theorem SetRel.comp_subset_self {α : Type u_1} {R : SetRel α α} [R.IsTrans] : R.comp R ⊆ R

theorem SetRel.comp_eq_self {α : Type u_1} {R : SetRel α α} [R.IsRefl] [R.IsTrans] : R.comp R = R

theorem SetRel.isTrans_iff_comp_subset_self {α : Type u_1} {R : SetRel α α} : R.IsTrans ↔ R.comp R ⊆ R

instance SetRel.isTrans_empty {α : Type u_1} : ∅.IsTrans

instance SetRel.isTrans_univ {α : Type u_1} : SetRel.IsTrans Set.univ

instance SetRel.isTrans_singleton {α : Type u_1} (x : α × α) : {x}.IsTrans

instance SetRel.isTrans_inter {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsTrans] [R₂.IsTrans] : (R₁ ∩ R₂).IsTrans

theorem SetRel.IsTrans.sInter {α : Type u_1} {ℛ : Set (SetRel α α)} (hℛ : ∀ (R : SetRel α α), R ∈ ℛ → R.IsTrans) : SetRel.IsTrans (⋂₀ ℛ)

instance SetRel.isTrans_iInter {α : Type u_1} {ι : Sort u_5} {R : ι → SetRel α α} [∀ (i : ι), (R i).IsTrans] : SetRel.IsTrans (⋂ (i : ι), R i)

instance SetRel.isTrans_id {α : Type u_1} : SetRel.id.IsTrans

instance SetRel.isTrans_preimage {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : β → α} [R.IsTrans] : SetRel.IsTrans (Prod.map f f ⁻¹' R)

instance SetRel.isTrans_symmetrize {α : Type u_1} {R : SetRel α α} [R.IsTrans] : R.symmetrize.IsTrans

@[reducible, inline]

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

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

Equations

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

theorem SetRel.irrefl {α : Type u_1} (R : SetRel α α) (a : α) [R.IsIrrefl] : ¬(a, a) ∈ R

instance SetRel.instIsIrreflSetOfProdMatch_1PropOfIrrefl {α : Type u_1} {R : α → α → Prop} [Std.Irrefl R] : SetRel.IsIrrefl {(a, b) : α × α | R a b}

@[reducible, inline]

abbrev SetRel.IsWellFounded {α : Type u_1} (R : SetRel α α) : 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 SetRel.Hom {α : Type u_1} {β : Type u_2} (R : SetRel α α) (S : SetRel β β) : 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 : α → β) : SetRel α β

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

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 = SetRel.id

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

def Function.tupleGraph {α : Type u_1} {β : Type u_2} (f : (α → β) → β) : Set (Option α → β)

The higher-arity graph of a function. Describes α-argument functions from β to β.

Equations

• Function.tupleGraph f = {v : Option α → β | f (v ∘ some) = v none}

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

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

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

@[reducible, inline]

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

A shorthand for α → β → Prop.

Consider using SetRel instead if you want extra API for relations.

Equations

• Rel α β = (α → β → Prop)