Documentation

Mathlib.Data.Rel

Relations #

This file defines bundled relations. A relation between α and β is a function α → β → Prop→ β → Prop→ Prop. Relations are also known as set-valued functions, or partial multifunctions.

Main declarations #

def Rel (α : Type u_1) (β : Type u_2) :
Type (maxu_1u_2)

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

Equations
instance instCompleteLatticeRel {α : Type u_1} {β : Type u_2} :
Equations
  • instCompleteLatticeRel = let_fun this := inferInstance; this
instance instInhabitedRel {α : Type u_1} {β : Type u_2} :
Inhabited (Rel α β)
Equations
  • instInhabitedRel = let_fun this := inferInstance; this
theorem Rel.ext {α : Type u_1} {β : Type u_2} {r : Rel α β} {s : Rel α β} :
(∀ (a : α), r a = s a) → r = s
def Rel.inv {α : Type u_1} {β : Type u_2} (r : Rel α β) :
Rel β α

The inverse relation : r.inv x y ↔ r y x↔ 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 : β) :
Rel.inv r y x r x y
theorem Rel.inv_inv {α : Type u_1} {β : Type u_2} (r : Rel α β) :
def Rel.dom {α : Type u_1} {β : Type u_2} (r : Rel α β) :
Set α

Domain of a relation

Equations
theorem Rel.dom_mono {α : Type u_1} {β : Type u_2} {r : Rel α β} {s : Rel α β} (h : r s) :
def Rel.codom {α : Type u_1} {β : Type u_2} (r : Rel α β) :
Set β

Codomain aka range of a relation

Equations
theorem Rel.codom_inv {α : Type u_1} {β : Type u_2} (r : Rel α β) :
theorem Rel.dom_inv {α : Type u_2} {β : Type u_1} (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 CategoryTheory/ order of arguments.

Equations
theorem Rel.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_1} (r : Rel α β) (s : Rel β γ) (t : Rel γ δ) :
@[simp]
theorem Rel.comp_right_id {α : Type u_1} {β : Type u_2} (r : Rel α β) :
Rel.comp r Eq = r
@[simp]
theorem Rel.comp_left_id {α : Type u_1} {β : Type u_2} (r : Rel α β) :
Rel.comp Eq r = r
theorem Rel.inv_id {α : Type u_1} :
Rel.inv Eq = Eq
theorem Rel.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : Rel α β) (s : Rel β γ) :
def Rel.image {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) :
Set β

Image of a set under a relation

Equations
theorem Rel.mem_image {α : Type u_1} {β : Type u_2} (r : Rel α β) (y : β) (s : Set α) :
y Rel.image r s x, x s r x y
theorem Rel.image_subset {α : Type u_1} {β : Type u_2} (r : Rel α β) :
((fun x x_1 => x x_1) fun x x_1 => x x_1) (Rel.image r) (Rel.image r)
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 : Set α) (t : Set α) :
theorem Rel.image_union {α : Type u_1} {β : Type u_2} (r : Rel α β) (s : Set α) (t : Set α) :
@[simp]
theorem Rel.image_id {α : Type u_1} (s : Set α) :
Rel.image Eq s = s
theorem Rel.image_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} (r : Rel α β) (s : Rel β γ) (t : Set α) :
theorem Rel.image_univ {α : Type u_2} {β : Type u_1} (r : Rel α β) :
Rel.image r Set.univ = Rel.codom r
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_2} {β : Type u_1} (r : Rel α β) (x : α) (s : Set β) :
x Rel.preimage r s y, y s r x y
theorem Rel.preimage_def {α : Type u_2} {β : Type u_1} (r : Rel α β) (s : Set β) :
Rel.preimage r s = { x | y, y s r x y }
theorem Rel.preimage_mono {α : Type u_2} {β : Type u_1} (r : Rel α β) {s : Set β} {t : Set β} (h : s t) :
theorem Rel.preimage_inter {α : Type u_2} {β : Type u_1} (r : Rel α β) (s : Set β) (t : Set β) :
theorem Rel.preimage_union {α : Type u_2} {β : Type u_1} (r : Rel α β) (s : Set β) (t : Set β) :
theorem Rel.preimage_id {α : Type u_1} (s : Set α) :
theorem Rel.preimage_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} (r : Rel α β) (s : Rel β γ) (t : Set γ) :
theorem Rel.preimage_univ {α : Type u_1} {β : Type u_2} (r : Rel α β) :
Rel.preimage r Set.univ = Rel.dom r
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
theorem Rel.mem_core {α : Type u_2} {β : Type u_1} (r : Rel α β) (x : α) (s : Set β) :
x Rel.core r s ∀ (y : β), r x yy s
theorem Rel.core_subset {α : Type u_2} {β : Type u_1} (r : Rel α β) :
((fun x x_1 => x x_1) fun x x_1 => x x_1) (Rel.core r) (Rel.core r)
theorem Rel.core_mono {α : Type u_2} {β : Type u_1} (r : Rel α β) :
theorem Rel.core_inter {α : Type u_2} {β : Type u_1} (r : Rel α β) (s : Set β) (t : Set β) :
Rel.core r (s t) = Rel.core r s Rel.core r t
theorem Rel.core_union {α : Type u_2} {β : Type u_1} (r : Rel α β) (s : Set β) (t : Set β) :
@[simp]
theorem Rel.core_univ {α : Type u_1} {β : Type u_2} (r : Rel α β) :
Rel.core r Set.univ = Set.univ
theorem Rel.core_id {α : Type u_1} (s : Set α) :
Rel.core Eq s = s
theorem Rel.core_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} (r : Rel α β) (s : Rel β γ) (t : Set γ) :
def Rel.restrictDomain {α : 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 β) :
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
theorem Set.image_eq {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
theorem Set.preimage_eq {α : Type u_2} {β : Type u_1} (f : αβ) (s : Set β) :
theorem Set.preimage_eq_core {α : Type u_2} {β : Type u_1} (f : αβ) (s : Set β) :