Theorem ciSup_ciSup_eq_left

Modification history

2026-07-23 15:44
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
feat(Order/ConditionallyCompleteLattice/Indexed): `iSup_iSup_eq_{left/right}` for `ConditionallyCompleteLinearOrderBot` (#38856) …
Added ciSup_ciSup_eq_leftView on Github →