This file defines bundled relations. A relation between
β is a function
α → β → Prop.
Relations are also known as set-valued functions, or partial multifunctions.
Main declarations #
Rel α β: Relation between
Rel β αobtained by swapping the arguments of
Rel.dom: Domain of a relation.
x ∈ r.domiff there exists
r x y.
Rel.codom: Codomain, aka range, of a relation.
y ∈ r.codomiff there exists
r x y.
Rel.comp: Relation composition. Note that the arguments order follows the
r.comp s x z ↔ ∃ y, r x y ∧ s y z.
Rel.image: Image of a set under a relation.
r.image sis the set of
f xover 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 sis the set of
x : αsuch that all
Rel.restrict_domain: Domain-restriction of a relation to a subtype.
Function.graph: Graph of a function as a relation.