Commit 2025-07-22 22:14 8b5f0856

View on Github →

chore(Order/Monotone/Basic): rename Monotone.eq_of_le_of_le (#27269) Monotone.eq_of_ge_of_le follows the new naming convention. Also remove a duplicate of lt_of_le_of_ne'.

Estimated changes

Modified Mathlib/Order/Monotone/Basic.lean

added theorem Antitone.eq_of_ge_of_le

deleted theorem Antitone.eq_of_le_of_le

added theorem Monotone.eq_of_ge_of_le

deleted theorem Monotone.eq_of_le_of_le

Modified Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

Modified Mathlib/Tactic/Linarith/Frontend.lean

Modified Mathlib/Tactic/Positivity/Core.lean

deleted theorem Mathlib.Meta.Positivity.lt_of_le_of_ne'