mathlib

91cc4ae6 - feat(order/category/BoundedOrder): The category of bounded orders (#11961)

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`.