Theorem Finset.sup_eq_zero

Modification history

2026-06-27 13:04
Mathlib/Algebra/Order/Monoid/Canonical/Basic.lean
feat(Topology/MetricSpace): the L^p direct sum of metric spaces (#40212) …
Deleted Finset.sup_eq_zeroView on Github →
2024-10-02 14:32
Mathlib/Algebra/Order/Monoid/Canonical/Basic.lean
feat: `Finset.sup s f = 0 ↔ ∀ i ∈ s, f i = 0` (#17078) …
Added Finset.sup_eq_zeroView on Github →