Relations

This file defines bundled relations. A relation between α and β is a function α → β → Prop→ β → Prop→ 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∈ r.dom iff there exists y such that r x y.
• Rel.codom: Codomain, aka range, of a relation. y ∈ r.codom∈ 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↔ ∃ y, r x y ∧ s y z∃ y, r x y ∧ s y z∧ 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∈ 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.

ink

def Rel (α : Type u_1) (β : Type u_2) : Type (maxu_1u_2)

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

Equations

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

ink

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

Equations

• instCompleteLatticeRel = let_fun this := inferInstance; this

ink

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

Equations

• instInhabitedRel = let_fun this := inferInstance; this

ink

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

ink

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

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

Equations

• Rel.inv r = flip r

ink

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

ink

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

ink

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

Domain of a relation

Equations

• Rel.dom r = { x | ∃ y, r x y }

ink

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

ink

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

Codomain aka range of a relation

Equations

• Rel.codom r = { y | ∃ x, r x y }

ink

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

ink

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

ink

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

• Rel.comp r s x z = ∃ y, r x y ∧ s y z

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

Image of a set under a relation

Equations

• Rel.image r s = { y | ∃ x, x ∈ s ∧ r x y }

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

• Rel.preimage r s = Rel.image (Rel.inv r) s

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

• Rel.core r s = { x | ∀ (y : β), r x y → y ∈ s }

ink

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

ink

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

ink

theorem Rel.core_mono {α : Type u_2} {β : Type u_1} (r : Rel α β) : Monotone (Rel.core r)

ink

theorem Rel.core_inter {α : Type u_2} {β : Type u_1} (r : Rel α β) (s : Set β) (t : Set β) : Rel.core r (s ∩ t) = Rel.core r s ∩ Rel.core r t

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

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

ink

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

ink

theorem Rel.image_core_gc {α : Type u_1} {β : Type u_2} (r : Rel α β) : GaloisConnection (Rel.image r) (Rel.core r)

ink

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)

ink

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

ink

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

ink

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