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 theRel β α
obtained by swapping the arguments ofr
.Rel.dom
: Domain of a relation.x ∈ r.dom
iff there existsy
such thatr x y
.Rel.codom
: Codomain, aka range, of a relation.y ∈ r.codom
iff there existsx
such thatr x y
.Rel.comp
: Relation composition. Note that the arguments order follows theCategoryTheory/
one, sor.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 off x
over allx ∈ s
.Rel.preimage
: Preimage of a set under a relation. Note thatr.preimage = r.inv.image
.Rel.core
: Core of a set. Fors : Set β
,r.core s
is the set ofx : α
such that ally
related tox
are ins
.Rel.restrict_domain
: Domain-restriction of a relation to a subtype.Function.graph
: Graph of a function as a relation.
TODO #
The Rel.comp
function uses the notation r • s
, rather than the more common r ∘ s
for things
named comp
. This is because the latter is already used for function composition, and causes a
clash. A better notation should be found, perhaps a variant of r ∘r s
or r; s
.
Equations
- instCompleteLatticeRel = inferInstance
theorem
Rel.image_core_gc
{α : Type u_1}
{β : Type u_2}
(r : Rel α β)
:
GaloisConnection r.image r.core
@[simp]
theorem
Function.graph_def
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(x : α)
(y : β)
:
Function.graph f x y ↔ f x = y
@[simp]
theorem
Function.graph_inj
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
:
Function.graph f = Function.graph g ↔ f = g
theorem
Function.graph_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : β → γ}
{g : α → β}
:
Function.graph (f ∘ g) = (Function.graph g).comp (Function.graph f)
theorem
Equiv.graph_inv
{α : Type u_1}
{β : Type u_2}
(f : α ≃ β)
:
Function.graph ⇑f.symm = (Function.graph ⇑f).inv
theorem
Relation.is_graph_iff
{α : Type u_1}
{β : Type u_2}
(r : Rel α β)
:
(∃! f : α → β, Function.graph f = r) ↔ ∀ (x : α), ∃! y : β, r x y
theorem
Set.image_eq
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set α)
:
f '' s = (Function.graph f).image s
theorem
Set.preimage_eq
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set β)
:
f ⁻¹' s = (Function.graph f).preimage s
theorem
Set.preimage_eq_core
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(s : Set β)
:
f ⁻¹' s = (Function.graph f).core s