mathlib documentation

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} (r : rel α β) :
rel β α

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

Equations
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
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
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.

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

The graph of a function as a relation.

Equations
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