mathlib documentation

order.category.BoundedOrder

The category of bounded orders #

This defines BoundedOrder, the category of bounded orders.

structure BoundedOrder  :
Type (u_1+1)

The category of bounded orders with monotone functions.

Instances for BoundedOrder
def BoundedOrder.of (α : Type u_1) [partial_order α] [bounded_order α] :

Construct a bundled BoundedOrder from a fintype partial_order.

Equations
@[simp]
theorem BoundedOrder.coe_of (α : Type u_1) [partial_order α] [bounded_order α] :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

order_dual as a functor.

Equations
def BoundedOrder.iso.mk {α β : BoundedOrder} (e : α ≃o β) :
α β

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

Equations
@[simp]
@[simp]