Extend a partial order to a linear order #
This file constructs a linear order which is an extension of the given partial order, using Zorn's lemma.
Any partial order can be extended to a linear order.
A type alias for α
, intended to extend a partial order on α
to a linear order.
Instances For
The embedding of α
into LinearExtension α
as a relation homomorphism.