English
Let s be a finite set of indices ι, and for each c ∈ s consider a finitely supported function h(c): α →₀ M. If a is in the support of the finite sum ∑_{c∈s} h(c), then there exists some c ∈ s with a ∈ support(h(c)).
Русский
Пусть s — конечное множество индексов ι, и для каждого c ∈ s задана конечноподдерживаемая функция h(c): α →₀ M. Если a лежит в опоре суммы ∑_{c∈s} h(c), то существует c ∈ s такое, что a ∈ опора h(c).
LaTeX
$$$a \in \operatorname{supp}\Bigl(\sum_{c \in s} h(c)\Bigr) \Rightarrow \exists c \in s,\ a \in \operatorname{supp}(h(c))$$$
Lean4
theorem mem_support_finset_sum [AddCommMonoid M] {s : Finset ι} {h : ι → α →₀ M} (a : α)
(ha : a ∈ (∑ c ∈ s, h c).support) : ∃ c ∈ s, a ∈ (h c).support :=
let ⟨_, hf, hfa⟩ := mem_support_multiset_sum a ha
let ⟨c, hc, Eq⟩ := Multiset.mem_map.1 hf
⟨c, hc, Eq.symm ▸ hfa⟩
