Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-02 08:53 a6d70aa7

View on Github →

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 α)

Estimated changes