Commit 2022-04-18 17:14 d89160b5

feat(order/bounded_order): Strictly monotone functions preserve maximality (#13434) Prove f a = f ⊤ ↔ a = ⊤ and f a = f ⊥ ↔ a = ⊥ for strictly monotone/antitone functions. Also fix is_max.eq_top and friends and delete eq_top_of_maximal (which accidentally survived the last refactor).