support_sum_subset — Mathlib

English

For a finite set of finsupps, the support of the sum equals the supremum over the supports of the elements.

Русский

Для конечного множества финспп опора суммы равна супремусу опор элементов.

LaTeX

$$$(s.sum id).\\\\support = Finset.sup s Finsupp\\\\support$$$

Lean4

theorem support_sum_subset [AddCommMonoid M] (s : Finset (ι →₀ M)) :
    (s.sum id).support ⊆ Finset.sup s Finsupp.support := by classical convert Multiset.support_sum_subset s.1; simp

Похожие утверждения