Commit 2025-07-10 15:23 cfc5f69e

View on Github →

chore(Order): use new ge/gt naming convention - Part 5 (#25586) This PR renames, moves around, and deprecates theorems about PartialOrders The main changes are in Mathlib.Order.Defs.PartialOrder and Mathlib.Order.Basic.

Estimated changes

modified theorem norm_eq_zero'
added theorem LE.le.ge_iff_eq'
deleted theorem LE.le.gt_iff_ne
deleted theorem LE.le.le_iff_eq
added theorem LE.le.lt_iff_ne'
deleted theorem LE.le.not_gt_iff_eq
added theorem LE.le.not_lt_iff_eq'
modified theorem eq_iff_le_not_lt
modified theorem eq_iff_not_lt_of_le
deleted theorem eq_of_ge_of_not_gt
added theorem eq_of_le_of_not_lt'
modified theorem eq_of_le_of_not_lt
deleted theorem eq_or_gt_of_le
added theorem eq_or_lt_of_le'
modified theorem eq_or_lt_of_le
deleted theorem gt_or_eq_of_le
added theorem lt_or_eq_of_le'
deleted theorem Decidable.eq_or_lt_of_le
deleted theorem Decidable.le_iff_lt_or_eq
deleted theorem Decidable.lt_or_eq_of_le
modified theorem UpperSet.lt_erase