data.rel

# 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.
@[protected, instance]
def rel.inhabited (α : Type u_1) (β : Type u_2) :
inhabited (rel α β)
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)
Instances for rel
@[protected, instance]
def rel.complete_lattice (α : Type u_1) (β : Type u_2) :
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
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} (r : rel α β) :
set α

Domain of a relation

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

Image of a set under a relation

Equations
• r.image s = {y : β | ∃ (x : α) (H : x s), r x y}
Instances for ↥rel.image
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 α) :
= s
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 α β) :
= r.codom
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
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 β} (h : s 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 α) :
= s
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 α β) :
= r.dom
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
• 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)
@[simp]
theorem rel.core_univ {α : Type u_1} {β : Type u_2} (r : rel α β) :
theorem rel.core_id {α : Type u_1} (s : set α) :
= s
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
• = λ (x : {x // x s}) (y : β), r x.val y
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.image_core_gc {α : Type u_1} {β : Type u_2} (r : rel α β) :
def function.graph {α : Type u_1} {β : Type u_2} (f : α → β) :
rel α β

The graph of a function as a relation.

Equations
• = λ (x : α) (y : β), f x = y
theorem set.image_eq {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :
f '' s = .image s
theorem set.preimage_eq {α : Type u_1} {β : Type u_2} (f : α → β) (s : set β) :
f ⁻¹' s = s
theorem set.preimage_eq_core {α : Type u_1} {β : Type u_2} (f : α → β) (s : set β) :
f ⁻¹' s = .core s