# Documentation

Mathlib.Order.Category.BddOrd

# The category of bounded orders #

This defines BddOrd, the category of bounded orders.

structure BddOrd :
Type (u_1 + 1)

The category of bounded orders with monotone functions.

• toPartOrd : PartOrd

The underlying object in the category of partial orders.

• isBoundedOrder : BoundedOrder s.toPartOrd
Instances For
Equations
• = X.toPartOrd.str
def BddOrd.of (α : Type u_1) [] [] :

Construct a bundled BddOrd from a Fintype PartialOrder.

Equations
Instances For
@[simp]
theorem BddOrd.coe_of (α : Type u_1) [] [] :
().toPartOrd = α
Equations
Equations
instance BddOrd.instFunLike (X : BddOrd) (Y : BddOrd) :
FunLike (X Y) X.toPartOrd fun (x : X.toPartOrd) => Y.toPartOrd
Equations
• = let_fun this := inferInstance; this
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem BddOrd.dual_map {X : BddOrd} {Y : BddOrd} (a : BoundedOrderHom X.toPartOrd Y.toPartOrd) :
BddOrd.dual.map a = BoundedOrderHom.dual a
@[simp]
theorem BddOrd.dual_obj (X : BddOrd) :
BddOrd.dual.obj X = BddOrd.of (X.toPartOrd)ᵒᵈ

OrderDual as a functor.

Equations
Instances For
@[simp]
theorem BddOrd.Iso.mk_hom {α : BddOrd} {β : BddOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
().hom = e
@[simp]
theorem BddOrd.Iso.mk_inv {α : BddOrd} {β : BddOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
().inv = ()
def BddOrd.Iso.mk {α : BddOrd} {β : BddOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
α β

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

Equations
Instances For

The equivalence between BddOrd and itself induced by OrderDual both ways.

Equations
• One or more equations did not get rendered due to their size.
Instances For