Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-03-17 20:24
191569ec
View on Github →
feat: biSup and biInf for monotone and antitone functions (
#22560
)
Estimated changes
Modified
Mathlib/Order/CompleteLattice.lean
added
theorem
biInf_ge_eq_of_monotone
added
theorem
biInf_le_eq_of_antitone
added
theorem
biSup_ge_eq_of_antitone
added
theorem
biSup_le_eq_of_monotone