Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-08-05 08:52
f74b424c
View on Github →
feat(ConditionallyCompleteLattice): ciSup_image, ciSup_or', and other iSup-like lemmas (
#15271
)
Estimated changes
Modified
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
added
theorem
ciInf_image
added
theorem
ciInf_subtype''
added
theorem
ciInf_subtype'
added
theorem
ciInf_subtype
added
theorem
ciSup_image
added
theorem
ciSup_or'
added
theorem
ciSup_subtype''
added
theorem
ciSup_subtype'
added
theorem
ciSup_subtype
added
theorem
csInf_image
added
theorem
csSup_image