The category of bounded orders with monotone functions.
- toPartOrd : PartOrd
The underlying object in the category of partial orders.
- isBoundedOrder : BoundedOrder ↑self.toPartOrd
Instances For
Equations
- BddOrd.instPartialOrderαToPartOrd X = X.toPartOrd.str
Construct a bundled BddOrd
from a Fintype
PartialOrder
.
Instances For
@[simp]
Equations
- BddOrd.instInhabitedBddOrd = { default := BddOrd.of PUnit.{u_1 + 1} }
Equations
- BddOrd.instFunLike X Y = let_fun this := inferInstance; this
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.
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
OrderDual
as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
BddOrd.Iso.mk_hom
{α : BddOrd}
{β : BddOrd}
(e : ↑α.toPartOrd ≃o ↑β.toPartOrd)
:
(BddOrd.Iso.mk e).hom = ↑e
@[simp]
theorem
BddOrd.Iso.mk_inv
{α : BddOrd}
{β : BddOrd}
(e : ↑α.toPartOrd ≃o ↑β.toPartOrd)
:
(BddOrd.Iso.mk e).inv = ↑(OrderIso.symm e)
Constructs an equivalence between bounded orders from an order isomorphism between them.
Equations
- BddOrd.Iso.mk e = { hom := ↑e, inv := ↑(OrderIso.symm e), hom_inv_id := ⋯, inv_hom_id := ⋯ }