mathlib3 documentation

order.category.FinPartOrd

The category of finite partial orders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This defines FinPartOrd, the category of finite partial orders.

Note: FinPartOrd is not a subcategory of BddOrd because finite orders are not necessarily bounded.

TODO #

FinPartOrd is equivalent to a small category.

@[protected, instance]
Equations
def FinPartOrd.of (α : Type u_1) [partial_order α] [fintype α] :

Construct a bundled FinPartOrd from fintype + partial_order.

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

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

Equations

order_dual as a functor.

Equations