English
For a finite set s and f : α → M, the support of the Finset sum ∑_{a∈s} f(a) lies inside the union of the supports of the summands.
Русский
Для конечного множества s и f: α → M опора суммы ∑_{a∈s} f(a) содержится в объединении опор самих слагаемых.
LaTeX
$$$$ \operatorname{supp}\left(\sum_{a\in s} f(a)\right) \subseteq \bigcup_{a\in s} \operatorname{supp}(f(a)). $$$$
Lean4
theorem support_finset_sum [DecidableEq β] [AddCommMonoid M] {s : Finset α} {f : α → β →₀ M} :
(Finset.sum s f).support ⊆ s.biUnion fun x => (f x).support :=
by
rw [← Finset.sup_eq_biUnion]
induction s using Finset.cons_induction_on with
| empty => rfl
| cons _ _ _ ih =>
rw [Finset.sum_cons, Finset.sup_cons]
exact support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)
