mathlib docs: data.rel

source

@[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

@[instance]

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

complete_lattice (rel α β)

source

def rel.inv {α : Type u_1} {β : Type u_2} :

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} :

rel α β → set α

Domain of a relation

Equations

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

source

def rel.codom {α : Type u_1} {β : Type u_2} :

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} :

rel α β → 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} :

rel α β → 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} :

rel α β → 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 β} :

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} :

rel α β → 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.

Equations

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

source

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

source

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

(has_subset.subset ⇒ has_subset.subset) r.core r.core

source

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

monotone r.core

source

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

r.core (s ∩ t) = r.core s ∩ r.core t

source

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

r.core s ∪ r.core t ⊆ r.core (s ∪ t)

source

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

r.core set.univ = set.univ

source

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

rel.core eq s = s

source

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)

source

def rel.restrict_domain {α : 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.restrict_domain s = λ (x : {x // x ∈ s}) (y : β), r x.val y

source

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

source

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

galois_connection r.image r.core

source

def function.graph {α : Type u_1} {β : Type u_2} :

(α → β) → rel α β

The graph of a function as a relation.

Equations

function.graph f = λ (x : α) (y : β), f x = y

source

theorem set.image_eq {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :

f '' s = (function.graph f).image s

source

theorem set.preimage_eq {α : Type u_1} {β : Type u_2} (f : α → β) (s : set β) :

f ⁻¹' s = (function.graph f).preimage s

source

theorem set.preimage_eq_core {α : Type u_1} {β : Type u_2} (f : α → β) (s : set β) :

f ⁻¹' s = (function.graph f).core s

mathlib documentation

data.rel

General documentation

Additional documentation

Library

mathlib documentation

data.​rel

General documentation

Additional documentation

Library

data.rel