English
The support of the sum f.sum g is contained in the union of supports of g(i,f(i)) over i in the support of f.
Русский
Поддержка суммы f.sum g содержится в объединении поддержек g(i, f(i)) по i из поддержки f.
LaTeX
$$$\\operatorname{Supp}(f.sum g) \\subseteq \\operatorname{Supp}(f) \\cup \\bigcup_{i} \\operatorname{Supp}(g(i,f(i)))$$$
Lean4
theorem support_sum {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [∀ i₁, Zero (β₁ i₁)]
[∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
{f : Π₀ i₁, β₁ i₁} {g : ∀ i₁, β₁ i₁ → Π₀ i, β i} :
(f.sum g).support ⊆ f.support.biUnion fun i => (g i (f i)).support :=
by
have : ∀ i₁ : ι, (f.sum fun (i : ι₁) (b : β₁ i) => (g i b) i₁) ≠ 0 → ∃ i : ι₁, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0 :=
fun i₁ h =>
let ⟨i, hi, Ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
⟨i, mem_support_iff.1 hi, Ne⟩
simpa [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply] using this
