Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-07-05 03:31
34a6a03c
View on Github →
feat(Order): StrictMono of UpperSet/LowerSet.Iic/Iio/Ici/Ioi (
#26756
)
Estimated changes
Modified
Mathlib/Order/UpperLower/Principal.lean
added
theorem
LowerSet.Iic_strictMono
added
theorem
LowerSet.Iio_strictMono
added
theorem
UpperSet.Ici_strictMono
added
theorem
UpperSet.Ioi_strictMono