mathlib documentation

order.category.FinPartialOrder

The category of finite partial orders #

This defines FinPartialOrder, the category of finite partial orders.

Note: FinPartialOrder is NOT a subcategory of BoundedOrder because its morphisms do not preserve and .

TODO #

FinPartialOrder is equivalent to a small category.

Construct a bundled FinPartialOrder from fintype + partial_order.

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

Constructs an isomorphism of finite partial orders from an order isomorphism between them.

Equations

order_dual as a functor.

Equations