Commit 2025-08-13 12:33 6d9f5dd1

View on Github →

chore(Order/Monotone/Basic): use new ge/gt naming convention (#28314) As suggested at #mathlib4 > naming convention for ≤ and < @ 💬

Estimated changes

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean

Modified Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

Modified Mathlib/Computability/AkraBazzi/AkraBazzi.lean

Modified Mathlib/Data/ENNReal/Inv.lean

Modified Mathlib/Data/EReal/Operations.lean

modified theorem EReal.neg_le_neg_iff

modified theorem EReal.neg_lt_neg_iff

Modified Mathlib/Data/Finsupp/Lex.lean

Modified Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/Order/Bounds/Image.lean

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/Order/Monotone/Basic.lean

added theorem StrictAnti.le_iff_ge

deleted theorem StrictAnti.le_iff_le

added theorem StrictAnti.lt_iff_gt

deleted theorem StrictAnti.lt_iff_lt

added theorem StrictAntiOn.le_iff_ge

deleted theorem StrictAntiOn.le_iff_le

added theorem StrictAntiOn.lt_iff_gt

deleted theorem StrictAntiOn.lt_iff_lt

Modified Mathlib/Order/WellFoundedSet.lean

Modified Mathlib/Topology/Metrizable/Uniformity.lean