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.

structure FinPartialOrder  :
Type (u_1+1)

The category of finite partial orders with monotone functions.

Instances for FinPartialOrder
def FinPartialOrder.of (α : Type u_1) [partial_order α] [fintype α] :

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