support_sum_subset — Mathlib

English

For any list of finsupps, the support of the sum is contained in the fold of pairwise unions of supports.

Русский

Для списка финспп справедливо: опора суммы содержится в свёртке попарных объединений опор компонентов.

LaTeX

$$$\\operatorname{supp}(\\\\operatorname{sum}\\\\ l) \\\\subseteq l\\\\.foldr (\\\\operatorname{support} \\\\sqcup \\\\cdot) \\\\emptyset$$$

Lean4

theorem support_sum_subset [AddZeroClass M] (l : List (ι →₀ M)) : l.sum.support ⊆ l.foldr (Finsupp.support · ⊔ ·) ∅ :=
  by
  induction l with
  | nil => simp
  | cons hd tl IH =>
    simp only [List.sum_cons]
    exact Finsupp.support_add.trans (Finset.union_subset_union Finset.Subset.rfl IH)

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