mathlib3
67488dff - refactor(order/minimals): Change definition to `a ≤ b → b ≤ a` (#16103)

Commit

3 years ago

refactor(order/minimals): Change definition to `a ≤ b → b ≤ a` (#16103) This matches `is_min`/`is_max` and will allow to smoothly restate Zorn's lemma using those.

Author

YaelDillies

Parents

c2c31b52

mathlib3 67488dff - refactor(order/minimals): Change definition to `a ≤ b → b ≤ a` (#16103)

mathlib3
67488dff - refactor(order/minimals): Change definition to `a ≤ b → b ≤ a` (#16103)