English
Let f : α →₀ M and g : α → M →₀ N with M, N additive. Then the support of the sum f.sum g is contained in the bi-union over a in supp(f) of the supports of g(a)(f(a)).
Русский
Пусть f : α →₀ M и g : α → M →₀ N, где M, N — аддитивные. Тогда опора суммы f.sum g ⊆ ⋃^{bi}_{a ∈ supp(f)} опора(g(a)(f(a))).
LaTeX
$$$$ \operatorname{supp}(f \sum g) \subseteq \bigcup_{a \in \operatorname{supp}(f)} \operatorname{supp}\bigl(g(a)(f(a))\bigr). $$$$
Lean4
theorem support_sum [DecidableEq β] [Zero M] [AddCommMonoid N] {f : α →₀ M} {g : α → M → β →₀ N} :
(f.sum g).support ⊆ f.support.biUnion fun a => (g a (f a)).support :=
by
have : ∀ c, (f.sum fun a b => g a b c) ≠ 0 → ∃ a, f a ≠ 0 ∧ ¬(g a (f a)) c = 0 := fun a₁ h =>
let ⟨a, ha, ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
⟨a, mem_support_iff.mp ha, ne⟩
simpa only [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply, exists_prop]
