# mathlibdocumentation

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
@[protected, instance]
def BoundedOrder.has_coe_to_sort  :
(Type u_1)
Equations
@[protected, instance]
Equations
def BoundedOrder.of (α : Type u_1)  :

Construct a bundled BoundedOrder from a fintype partial_order.

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

order_dual as a functor.

Equations
@[simp]
@[simp]
theorem BoundedOrder.dual_map (X Y : BoundedOrder) (ᾰ : Y) :
def BoundedOrder.iso.mk {α β : BoundedOrder} (e : α ≃o β) :
α β

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

Equations
@[simp]
theorem BoundedOrder.iso.mk_inv {α β : BoundedOrder} (e : α ≃o β) :
= (e.symm)
@[simp]
theorem BoundedOrder.iso.mk_hom {α β : BoundedOrder} (e : α ≃o β) :
= e
@[simp]
@[simp]

The equivalence between BoundedOrder and itself induced by order_dual both ways.

Equations