Commit 2026-07-23 15:44 bd913bfd

View on Github →

feat(Order/ConditionallyCompleteLattice/Indexed): iSup_iSup_eq_{left/right} for ConditionallyCompleteLinearOrderBot (#38856) and ≤ versions for ConditionallyCompleteLattice.

Estimated changes

Modified Mathlib/Order/CompleteLattice/Basic.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

added theorem ciInf_ciInf_eq_left_le

added theorem ciInf_ciInf_eq_right_le

added theorem ciSup_ciSup_eq_left

added theorem ciSup_ciSup_eq_right

added theorem le_ciSup_ciSup_eq_left

added theorem le_ciSup_ciSup_eq_right