Theorem Finset.sup_univ_eq_ciSup

Modification history

2026-08-10 13:55

Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

feat(Order/ConditionallyCompleteLattice/Finset): add `sup_eq_ciSup` (#41361) …

Modified Finset.sup_univ_eq_ciSup View on Github →

2024-01-17 17:22

Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

feat(Analysis/NormedSpace/{ProdLp,PiLp}): add `BoundedSMul` instances (#9796) …

Added Finset.sup_univ_eq_ciSup View on Github →