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
- X.instPartialOrderαToPartOrd = X.toPartOrd.str
Construct a bundled BddOrd
from a Fintype
PartialOrder
.
Instances For
@[simp]
Equations
- BddOrd.instInhabited = { default := BddOrd.of PUnit.{?u.3 + 1} }
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
- BddOrd.dual = { obj := fun (X : BddOrd) => BddOrd.of (↑X.toPartOrd)ᵒᵈ, map := fun {X Y : BddOrd} => ⇑BoundedOrderHom.dual, map_id := BddOrd.dual.proof_1, map_comp := @BddOrd.dual.proof_2 }
Instances For
@[simp]
theorem
BddOrd.Iso.mk_inv
{α : BddOrd}
{β : BddOrd}
(e : ↑α.toPartOrd ≃o ↑β.toPartOrd)
:
(BddOrd.Iso.mk e).inv = ↑e.symm
@[simp]
theorem
BddOrd.Iso.mk_hom
{α : BddOrd}
{β : BddOrd}
(e : ↑α.toPartOrd ≃o ↑β.toPartOrd)
:
(BddOrd.Iso.mk e).hom = ↑e
Constructs an equivalence between bounded orders from an order isomorphism between them.
Equations
- BddOrd.Iso.mk e = { hom := ↑e, inv := ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }