Theorem ciSup_sup_eq

Modification history

2026-05-15 11:00
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
feat(Order/ConditionallyCompleteLattice/Indexed): `iSup` of `sup`s vs `sup` of `iSup`s (#36169) …
Added ciSup_sup_eqView on Github →