mathlib documentation

order.category.PartialOrder

Category of partial orders #

This defines PartialOrder, the category of partial orders with monotone maps.

def PartialOrder.of (α : Type u_1) [partial_order α] :

Construct a bundled PartialOrder from the underlying type and typeclass.

Equations
@[simp]
theorem PartialOrder.coe_of (α : Type u_1) [partial_order α] :
@[protected, instance]
Equations
@[simp]
def PartialOrder.iso.mk {α β : PartialOrder} (e : α ≃o β) :
α β

Constructs an equivalence between partial orders from an order isomorphism between them.

Equations
@[simp]

order_dual as a functor.

Equations

antisymmetrization as a functor. It is the free functor.

Equations