mathlib

56d6a915 - chore(order/basic): Rename `no_bot_order`/`no_top_order` to `no_min_order`/`no_max_order` (#11357)

chore(order/basic): Rename `no_bot_order`/`no_top_order` to `no_min_order`/`no_max_order` (#11357) because that's really what they are. `∀ a, ∃ b, b < a` precisely means that every `a` is not a minimal element. The correct statement for an order without bottom elements is `∀ a, ∃ b, ¬ a ≤ b`, which is a weaker condition in general. Both conditions are equivalent over a linear order. Renames * `no_bot_order` -> `no_min_order` * `no_top_order` -> `no_max_order` * `no_bot` -> `exists_lt` * `no_top` -> `exists_gt`