# mathlib3documentation

order.category.BddOrd

# The category of bounded orders #

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

This defines BddOrd, the category of bounded orders.

structure BddOrd  :
Type (u_1+1)

The category of bounded orders with monotone functions.

Instances for BddOrd
@[protected, instance]
Equations
@[protected, instance]
Equations
def BddOrd.of (α : Type u_1)  :

Construct a bundled BddOrd from a fintype partial_order.

Equations
@[simp]
theorem BddOrd.coe_of (α : Type u_1)  :
(BddOrd.of α) = α
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
def BddOrd.dual  :

order_dual as a functor.

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

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

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

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

Equations