Commit 2022-01-11 13:55 56d6a915
View on Github →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