Relations

This file defines bundled relations. A relation between α and β is a function α → β → Prop. Relations are also known as set-valued functions, or partial multifunctions.

Main declarations

• Rel α β: Relation between α and β.
• Rel.inv: r.inv is the Rel β α obtained by swapping the arguments of r.
• Rel.dom: Domain of a relation. x ∈ r.dom iff there exists y such that r x y.
• Rel.codom: Codomain, aka range, of a relation. y ∈ r.codom iff there exists x such that r x y.
• Rel.comp: Relation composition. Note that the arguments order follows the CategoryTheory/ one, so r.comp s x z ↔ ∃ y, r x y ∧ s y z.
• Rel.image: Image of a set under a relation. r.image s is the set of f x over all x ∈ s.
• Rel.preimage: Preimage of a set under a relation. Note that r.preimage = r.inv.image.
• Rel.core: Core of a set. For s : Set β, r.core s is the set of x : α such that all y related to x are in s.
• Rel.restrict_domain: Domain-restriction of a relation to a subtype.
• Function.graph: Graph of a function as a relation.

TODOs

The Rel.comp function uses the notation r • s, rather than the more common r ∘ s for things named comp. This is because the latter is already used for function composition, and causes a clash. A better notation should be found, perhaps a variant of r ∘r s or r; s.

def Rel (α : Type u_4) (β : Type u_5) : Type (max u_4 u_5)

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

Equations

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

instance instCompleteLatticeRel {α : Type u_1} {β : Type u_2} : CompleteLattice (Rel α β)

Equations

• instCompleteLatticeRel = let_fun this := inferInstance; this

instance instInhabitedRel {α : Type u_1} {β : Type u_2} : Inhabited (Rel α β)

Equations

• instInhabitedRel = let_fun this := inferInstance; this

theorem Rel.ext {α : Type u_1} {β : Type u_2} {r : Rel α β} {s : Rel α β} : (∀ (a : α), r a = s a) → r = s

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 = flip r

theorem Rel.inv_def {α : Type u_1} {β : Type u_2} (r : Rel α β) (x : α) (y : β) : r.inv y x ↔ r x y

theorem Rel.inv_inv {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.inv.inv = r

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

Domain of a relation

Equations

• r.dom = {x : α | ∃ (y : β), r x y}

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

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

Codomain aka range of a relation

Equations

• r.codom = {y : β | ∃ (x : α), r x y}

theorem Rel.codom_inv {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.inv.codom = r.dom

theorem Rel.dom_inv {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.inv.dom = r.codom

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

Composition of relation; note that it follows the CategoryTheory/ order of arguments.

Equations

• r.comp s x z = ∃ (y : β), r x y ∧ s y z

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_right_id {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.comp Eq = r

@[simp]

theorem Rel.comp_left_id {α : Type u_1} {β : Type u_2} (r : Rel α β) : Rel.comp Eq r = r

@[simp]

theorem Rel.comp_right_bot {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) : r.comp ⊥ = ⊥

@[simp]

theorem Rel.comp_left_bot {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) : ⊥.comp r = ⊥

@[simp]

theorem Rel.comp_right_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) : r.comp ⊤ = fun (x : α) (x_1 : γ) => x ∈ r.dom

@[simp]

theorem Rel.comp_left_top {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) : ⊤.comp r = fun (x : γ) (y : β) => y ∈ r.codom

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

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.inv_bot {α : Type u_1} {β : Type u_2} : ⊥.inv = ⊥

@[simp]

theorem Rel.inv_top {α : Type u_1} {β : Type u_2} : ⊤.inv = ⊤

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 = {y : β | ∃ x ∈ s, r x y}

theorem Rel.mem_image {α : Type u_1} {β : Type u_2} (r : Rel α β) (y : β) (s : Set α) : y ∈ r.image s ↔ ∃ x ∈ s, r x y

theorem Rel.image_subset {α : Type u_1} {β : Type u_2} (r : Rel α β) : ((fun (x x_1 : Set α) => x ⊆ x_1) ⇒ fun (x x_1 : Set β) => x ⊆ x_1) r.image r.image

theorem Rel.image_mono {α : Type u_1} {β : Type u_2} (r : Rel α β) : Monotone r.image

theorem Rel.image_inter {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) (t : Set α) : r.image (s ∩ t) ⊆ r.image s ∩ r.image t

theorem Rel.image_union {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) (t : Set α) : r.image (s ∪ t) = r.image s ∪ r.image t

@[simp]

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

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

theorem Rel.image_univ {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.image Set.univ = r.codom

@[simp]

theorem Rel.image_empty {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.image ∅ = ∅

@[simp]

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

@[simp]

theorem Rel.image_top {α : Type u_1} {β : Type u_2} {s : Set α} (h : s.Nonempty) : ⊤.image s = Set.univ

def Rel.preimage {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) : Set α

Preimage of a set under a relation r. Same as the image of s under r.inv

Equations

• r.preimage s = r.inv.image s

theorem Rel.mem_preimage {α : Type u_1} {β : Type u_2} (r : Rel α β) (x : α) (s : Set β) : x ∈ r.preimage s ↔ ∃ y ∈ s, r x y

theorem Rel.preimage_def {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) : r.preimage s = {x : α | ∃ y ∈ s, r x y}

theorem Rel.preimage_mono {α : Type u_1} {β : Type u_2} (r : Rel α β) {s : Set β} {t : Set β} (h : s ⊆ t) : r.preimage s ⊆ r.preimage t

theorem Rel.preimage_inter {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) (t : Set β) : r.preimage (s ∩ t) ⊆ r.preimage s ∩ r.preimage t

theorem Rel.preimage_union {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) (t : Set β) : r.preimage (s ∪ t) = r.preimage s ∪ r.preimage t

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

theorem Rel.preimage_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) (s : Rel β γ) (t : Set γ) : (r.comp s).preimage t = r.preimage (s.preimage t)

theorem Rel.preimage_univ {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.preimage Set.univ = r.dom

@[simp]

theorem Rel.preimage_empty {α : Type u_1} {β : Type u_2} (r : Rel α β) : r.preimage ∅ = ∅

@[simp]

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

@[simp]

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

@[simp]

theorem Rel.preimage_top {α : Type u_1} {β : Type u_2} {s : Set β} (h : s.Nonempty) : ⊤.preimage s = Set.univ

theorem Rel.image_eq_dom_of_codomain_subset {α : Type u_1} {β : Type u_2} (r : Rel α β) {s : Set β} (h : r.codom ⊆ s) : r.preimage s = r.dom

theorem Rel.preimage_eq_codom_of_domain_subset {α : Type u_1} {β : Type u_2} (r : Rel α β) {s : Set α} (h : r.dom ⊆ s) : r.image s = r.codom

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

@[simp]

theorem Rel.preimage_inter_codom_eq {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) : r.preimage (s ∩ r.codom) = r.preimage s

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.image_preimage_subset_inter_codom {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) : s ∩ r.codom ⊆ r.image (r.preimage s)

def Rel.core {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : 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 s = {x : α | ∀ (y : β), r x y → y ∈ s}

theorem Rel.mem_core {α : Type u_1} {β : Type u_2} (r : Rel α β) (x : α) (s : Set β) : x ∈ r.core s ↔ ∀ (y : β), r x y → y ∈ s

theorem Rel.core_subset {α : Type u_1} {β : Type u_2} (r : Rel α β) : ((fun (x x_1 : Set β) => x ⊆ x_1) ⇒ fun (x x_1 : Set α) => x ⊆ x_1) r.core r.core

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 α β) (s : Set β) (t : Set β) : r.core (s ∩ t) = r.core s ∩ r.core t

theorem Rel.core_union {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set β) (t : Set β) : r.core s ∪ r.core t ⊆ r.core (s ∪ t)

@[simp]

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

theorem Rel.core_id {α : Type u_1} (s : Set α) : Rel.core Eq s = s

theorem Rel.core_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) (s : Rel β γ) (t : Set γ) : (r.comp s).core t = r.core (s.core t)

def Rel.restrictDomain {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) : Rel { x : α // x ∈ s } β

Restrict the domain of a relation to a subtype.

Equations

• r.restrictDomain s x y = r (↑x) y

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 Function.graph {α : Type u_1} {β : Type u_2} (f : α → β) : Rel α β

The graph of a function as a relation.

Equations

• Function.graph f x y = (f x = y)

@[simp]

theorem Function.graph_def {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) (y : β) : Function.graph f x y ↔ f x = y

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

@[simp]

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

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

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

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

theorem Relation.is_graph_iff {α : Type u_1} {β : Type u_2} (r : Rel α β) : (∃! f : α → β, Function.graph f = r) ↔ ∀ (x : α), ∃! y : β, r x y

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