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: SetRel composition. Note that the arguments order follows the category theory convention, namely (R ○ S) a c ↔ ∃ b, a ~[R] b ∧ b ~[S] c.
• 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 set of pairs SetRel α β with dedicated operations and API.

The function representation is lightweight and has native support from core Lean features. It is a good fit when a relation is primarily applied to two arguments. The set-of-pairs representation is useful when the relation itself is manipulated as a mathematical object, as R is in the examples below, because the standard Set API applies directly. For example:

• the inverse relation is the preimage Prod.swap ⁻¹' R;
• transporting a relation along f : α → γ and g : β → δ is the image (Prod.map f g) '' R;
• unions, intersections, complements, and the subset order are inherited from Set.

These operations can also be defined for α → β → Prop; the advantage of SetRel is reuse of the existing set API and direct interoperability with objects such as filters on α × α, rather than additional expressive power. SetRel also provides dedicated relational operations, including the notation ○ for composition. (Note that ○ is not function 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 it as

abbrev SetRel (α β : Type*) := Set (α × β)

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 α β} {s : Set α} (h : R.dom ⊆ s) : R.image s = R.cod

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

theorem SetRel.preimage_eq_image {α : Type u_1} {s : Set α} {R : SetRel α α} [R.IsSymm] : R.preimage s = R.image s

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.instIsTransOfPredProdMatch_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.instIsIrreflOfPredProdMatch_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)