mathlib documentation

data.rel

@[instance]
def rel.inhabited (α : Type u_1) (β : Type u_2) :
inhabited (rel α β)

def rel  :
Type u_1Type u_2Type (max u_1 u_2)

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

Equations
  • rel α β = (α → β → Prop)
@[instance]
def rel.complete_lattice (α : Type u_1) (β : Type u_2) :

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

Domain of a relation

Equations
  • r.dom = {x : α | ∃ (y : β), r x y}
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}
theorem rel.codom_inv {α : Type u_1} {β : Type u_2} (r : rel α β) :

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

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
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 α β) :

theorem rel.inv_id {α : Type u_1} :

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

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

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

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

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

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

@[simp]
theorem rel.image_id {α : Type u_1} (s : set α) :

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 α β) :

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

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}

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

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

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

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

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 α β) :

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 yy s}
theorem rel.mem_core {α : Type u_1} {β : Type u_2} (r : rel α β) (x : α) (s : set β) :
x r.core s ∀ (y : β), r x yy s

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

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

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

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)

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

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

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.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
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.core_preimage_gc {α : Type u_1} {β : Type u_2} (r : rel α β) :

def function.graph {α : Type u_1} {β : Type u_2} :
(α → β)rel α β

The graph of a function as a relation.

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

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

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