Commit 2022-08-20 13:58 67488dff

View on Github →

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.

Estimated changes

Modified src/order/minimal.lean

added theorem eq_of_mem_maximals

added theorem eq_of_mem_minimals

modified theorem is_greatest.mem_maximals

modified theorem is_least.mem_minimals

modified def maximals

modified theorem maximals_antichain

modified theorem maximals_mono

modified def minimals

modified theorem minimals_antichain

modified theorem minimals_mono