Commit 2022-02-12 09:20 91cc4ae6

View on Github →

feat(order/category/BoundedOrder): The category of bounded orders (#11961) Define BoundedOrder, the category of bounded orders with bounded order homs along with its forgetful functors to PartialOrder and Bipointed.

Estimated changes

Created src/order/category/BoundedOrder.lean

added def BoundedOrder.dual

added def BoundedOrder.dual_equiv

added def BoundedOrder.iso.mk

added def BoundedOrder.of

added structure BoundedOrder

added theorem BoundedOrder_dual_comp_forget_to_Bipointed

added theorem BoundedOrder_dual_comp_forget_to_PartialOrder

Modified src/order/category/PartialOrder.lean

deleted theorem PartialOrder_dual_equiv_comp_forget_to_Preorder

added theorem PartialOrder_to_dual_comp_forget_to_Preorder

Modified src/order/hom/bounded.lean