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 category_theory/ 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.

source

@[protected, instance]

def rel.inhabited (α : Type u_1) (β : Type u_2) :

inhabited (rel α β)

source

def rel (α : Type u_1) (β : Type u_2) :

Type (max u_1 u_2)

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

Equations

rel α β = (α → β → Prop)

source

@[protected, instance]

def rel.complete_lattice (α : Type u_1) (β : Type u_2) :

complete_lattice (rel α β)

source

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

source

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

r.inv y x ↔ r x y

source

theorem rel.inv_inv {α : Type u_1} {β : Type u_2} (r : rel α β) :

r.inv.inv = r

source

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

set α

Domain of a relation

Equations

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

source

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

r.dom ⊆ s.dom

source

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}

source

theorem rel.codom_inv {α : Type u_1} {β : Type u_2} (r : rel α β) :

r.inv.codom = r.dom

source

theorem rel.dom_inv {α : Type u_1} {β : Type u_2} (r : rel α β) :

r.inv.dom = r.codom

source

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 category_theory/ order of arguments.

Equations

r.comp s = λ (x : α) (z : γ), ∃ (y : β), r x y ∧ s y z

source

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)

source

@[simp]

theorem rel.comp_right_id {α : Type u_1} {β : Type u_2} (r : rel α β) :

r.comp eq = r

source

@[simp]

theorem rel.comp_left_id {α : Type u_1} {β : Type u_2} (r : rel α β) :

rel.comp eq r = r

source

theorem rel.inv_id {α : Type u_1} :

rel.inv eq = eq

source

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

source

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 : α) (H : x ∈ s), r x y}

source

theorem rel.mem_image {α : Type u_1} {β : Type u_2} (r : rel α β) (y : β) (s : set α) :

y ∈ r.image s ↔ ∃ (x : α) (H : x ∈ s), r x y

source

theorem rel.image_subset {α : Type u_1} {β : Type u_2} (r : rel α β) :

(has_subset.subset ⇒ has_subset.subset) r.image r.image

source

theorem rel.image_mono {α : Type u_1} {β : Type u_2} (r : rel α β) :

monotone r.image

source

theorem rel.image_inter {α : Type u_1} {β : Type u_2} (r : rel α β) (s t : set α) :

r.image (s ∩ t) ⊆ r.image s ∩ r.image t

source

theorem rel.image_union {α : Type u_1} {β : Type u_2} (r : rel α β) (s t : set α) :

r.image (s ∪ t) = r.image s ∪ r.image t

source

@[simp]

theorem rel.image_id {α : Type u_1} (s : set α) :

rel.image eq s = s

source

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)

source

theorem rel.image_univ {α : Type u_1} {β : Type u_2} (r : rel α β) :

r.image set.univ = r.codom

source

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

source

theorem rel.mem_preimage {α : Type u_1} {β : Type u_2} (r : rel α β) (x : α) (s : set β) :

x ∈ r.preimage s ↔ ∃ (y : β) (H : y ∈ s), r x y

source

theorem rel.preimage_def {α : Type u_1} {β : Type u_2} (r : rel α β) (s : set β) :

r.preimage s = {x : α | ∃ (y : β) (H : y ∈ s), r x y}

source

theorem rel.preimage_mono {α : Type u_1} {β : Type u_2} (r : rel α β) {s t : set β} (h : s ⊆ t) :

r.preimage s ⊆ r.preimage t

source

theorem rel.preimage_inter {α : Type u_1} {β : Type u_2} (r : rel α β) (s t : set β) :

r.preimage (s ∩ t) ⊆ r.preimage s ∩ r.preimage t

source

theorem rel.preimage_union {α : Type u_1} {β : Type u_2} (r : rel α β) (s t : set β) :

r.preimage (s ∪ t) = r.preimage s ∪ r.preimage t

source

theorem rel.preimage_id {α : Type u_1} (s : set α) :

rel.preimage eq s = s

source

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)

source

theorem rel.preimage_univ {α : Type u_1} {β : Type u_2} (r : rel α β) :

r.preimage set.univ = r.dom

source

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