Theorem ciSup_ciSup_eq_right

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_rightView on Github →