Theorem Finset.sup'_eq_one

Modification history

2026-06-27 13:04
Mathlib/Data/Finset/Lattice/Fold.lean
feat(Topology/MetricSpace): the L^p direct sum of metric spaces (#40212) …
Added Finset.sup'_eq_oneView on Github →