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.