English
If a list of finsupps is pairwise disjoint in their supports, then the support of the sum equals the fold of pairwise unions of supports.
Русский
Если список финспп попарочно несовместим по опорам, то опора суммы равна свёртке попарных объединений опор.
LaTeX
$$$l.\\\\operatorname{Pairwise} (\\\\operatorname{Disjoint} on Finsupp.\\\\operatorname{support}) \\\\Rightarrow \\\\operatorname{supp}(l.\\\\sum) = l.\\\\foldr (\\\\lambda s t, s \\\\uplus t) \\\\emptyset$$$
Lean4
theorem support_sum_eq [AddZeroClass M] (l : List (ι →₀ M)) (hl : l.Pairwise (_root_.Disjoint on Finsupp.support)) :
l.sum.support = l.foldr (Finsupp.support · ⊔ ·) ∅ := by
induction l with
| nil => simp
| cons hd tl IH =>
simp only [List.pairwise_cons] at hl
simp only [List.sum_cons, List.foldr_cons]
rw [Finsupp.support_add_eq, IH hl.right, Finset.sup_eq_union]
suffices _root_.Disjoint hd.support (tl.foldr (fun x y ↦ (Finsupp.support x ⊔ y)) ∅) by
exact Finset.disjoint_of_subset_right (List.support_sum_subset _) this
rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset, Finset.disjoint_sup_right]
intro f hf
simp only [List.mem_toFinset, List.mem_map] at hf
obtain ⟨f, hf, rfl⟩ := hf
exact hl.left _ hf
