Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-12-04 02:49
14ff892a
View on Github →
chore(Order/Defs/Unbundled): use
to_dual
(
#32378
) Note:
The name translations upper ↔ lower, and minimal ↔ maximal have been added.
Estimated changes
Modified
Mathlib/Order/Defs/Unbundled.lean
deleted
def
IsLowerSet
deleted
def
IsRelLowerSet
deleted
theorem
Maximal.le_of_ge
deleted
theorem
Maximal.prop
deleted
def
Maximal
deleted
theorem
MaximalFor.le_of_le
deleted
theorem
MaximalFor.prop
deleted
def
MaximalFor
Modified
Mathlib/Tactic/Translate/ToDual.lean