Turning a preorder into a partial order #
This file allows to make a preorder into a partial order by quotienting out the elements a
, b
such that a ≤ b
and b ≤ a
.
Antisymmetrization
is a functor from Preorder
to PartialOrder
. See Preorder_to_PartialOrder
.
Main declarations #
AntisymmRel
: The antisymmetrization relation.AntisymmRel r a b
means thata
andb
are related both ways byr
.Antisymmetrization α r
: The quotient ofα
byAntisymmRel r
. Even whenr
is just a preorder,Antisymmetrization α
is a partial order.
The antisymmetrization relation.
Instances For
Alias of the forward direction of antisymmRel_iff_eq
.
The antisymmetrization relation as an equivalence relation.
Instances For
The partial order derived from a preorder by making pairwise comparable elements equal. This is
the quotient by fun a b => a ≤ b ∧ b ≤ a
.
Instances For
Turn an element into its antisymmetrization.
Instances For
Get a representative from the antisymmetrization.
Instances For
Turns an order homomorphism from α
to β
into one from Antisymmetrization α
to
Antisymmetrization β
. Antisymmetrization
is actually a functor. See Preorder_to_PartialOrder
.
Instances For
ofAntisymmetrization
as an order embedding.
Instances For
Antisymmetrization
and orderDual
commute.