Commit 2024-10-02 14:32 8a443b7a

View on Github →

feat: Finset.sup s f = 0 ↔ ∀ i ∈ s, f i = 0 (#17078) From ForbiddenMatrix

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Monoid/Canonical/Basic.lean

added theorem Finset.sup'_eq_zero

added theorem Finset.sup_eq_zero