mathlib3

a6d70aa7 - feat(order/category/*): `order_dual` as an equivalence of categories (#11743)

feat(order/category/*): `order_dual` as an equivalence of categories (#11743) For `whatever` a category of orders, define * `whatever.iso_of_order_iso`: Turns an order isomorphism into an equivalence of objects inside `whatever` * `whatever.to_dual`: `order_dual` as a functor from `whatever` to itself * `whatever.dual_equiv`: The equivalence of categories between `whatever` and itself induced by `order_dual` both ways * `order_iso.dual_dual`: The order isomorphism between `α` and `order_dual (order_dual α)`