Commit 2024-10-22 11:41 e5f55855

View on Github →

feat(Order/ConditionallyCompleteLattice): lt_ciSup_iff and variants (#17965)

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem ciInf_lt_iff

added theorem csInf_lt_iff

added theorem lt_ciSup_iff'

added theorem lt_ciSup_iff

added theorem lt_csSup_iff'

added theorem lt_csSup_iff

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean