mathlib3

d89160b5 - feat(order/bounded_order): Strictly monotone functions preserve maximality (#13434)

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