Commit 2024-08-15 15:27 8e91009d

View on Github →

chore: Fix statement of eq_iff_not_lt_of_le (#15829) The statement said (a ≤ b → b = a) ↔ ¬a < b instead of the intended a ≤ b → (b = a ↔ ¬a < b). While both are true, the latter is the more useful one. Also pull out a PartialOrder section.

Estimated changes

modified theorem Ne.le_iff_lt
modified theorem Ne.not_le_or_not_le
modified theorem eq_iff_le_not_lt
modified theorem eq_iff_not_lt_of_le
modified theorem eq_of_ge_of_not_gt
modified theorem eq_of_le_of_not_lt
modified theorem eq_or_gt_of_le
modified theorem eq_or_lt_of_le
modified theorem gt_or_eq_of_le
modified theorem le_iff_eq_or_lt
modified theorem lt_iff_le_and_ne
modified theorem ne_iff_lt_iff_le