Commit 2025-07-27 02:05 db49903d

View on Github →

chore: chore(Order): use new ge/gt - Part 6 (#27528) This PR fixes 2 more order names: forall_ge_iff_le now aligns with le_of_forall_ge. And I think I made an error when applying the new naming convention for eq_or_lt_of_not_gt.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

Modified Mathlib/Order/Basic.lean

added theorem forall_ge_iff_le

deleted theorem forall_le_iff_ge

Modified Mathlib/Order/Defs/LinearOrder.lean

added theorem eq_or_gt_of_not_lt

deleted theorem eq_or_lt_of_not_gt