English
Let s be a finite multiset of finitely supported functions f: α →₀ M, where M is an additive commutative monoid. If a ∈ α lies in the support of the sum of all f in s, then there exists at least one f ∈ s such that a lies in the support of f.
Русский
Пусть s — конечная мультисистема функций f: α →₀ M, где M — добавочное коммутативное моноид. Если a ∈ α принадлежит поддержке суммы всех f из s, то существует хотя бы одна функция f в s такая, что a принадлежит поддержке f.
LaTeX
$$$a \in \operatorname{supp}\Bigl(\sum_{f \in s} f\Bigr) \implies \exists f \in s,\ a \in \operatorname{supp}(f)$$$
Lean4
theorem mem_support_multiset_sum [AddCommMonoid M] {s : Multiset (α →₀ M)} (a : α) :
a ∈ s.sum.support → ∃ f ∈ s, a ∈ (f : α →₀ M).support :=
Multiset.induction_on s (fun h => False.elim (by simp at h))
(by
intro f s ih ha
by_cases h : a ∈ f.support
· exact ⟨f, Multiset.mem_cons_self _ _, h⟩
· simp_rw [Multiset.sum_cons, mem_support_iff, add_apply, notMem_support_iff.1 h, zero_add] at ha
rcases ih (mem_support_iff.2 ha) with ⟨f', h₀, h₁⟩
exact ⟨f', Multiset.mem_cons_of_mem h₀, h₁⟩)
