English
If a multiset of finsupps is pairwise disjoint in supports, the sum’s support equals the supremum of mapped supports.
Русский
Если мультимножество финспп попарочно несовместимо по опорам, опора суммы равна супремусу опор.
LaTeX
$$$s.\\\\operatorname{Pairwise} (\\\\operatorname{Disjoint} on Finsupp.\\\\operatorname{support}) \\\\Rightarrow \\\\operatorname{supp}(s.\\\\operatorname{sum}) = (s.\\\\operatorname{map} Finsupp.\\\\operatorname{support}).\\\\operatorname{sup}$$$
Lean4
theorem support_sum_eq [AddCommMonoid M] (s : Multiset (ι →₀ M))
(hs : s.Pairwise (_root_.Disjoint on Finsupp.support)) : s.sum.support = (s.map Finsupp.support).sup :=
by
induction s using Quot.inductionOn with
| _ a
obtain ⟨l, hl, hd⟩ := hs
suffices a.Pairwise (_root_.Disjoint on Finsupp.support)
by
convert List.support_sum_eq a this
dsimp only [Function.comp_def]
simp only [quot_mk_to_coe'', map_coe, sup_coe, Finset.sup_eq_union, Finset.bot_eq_empty, List.foldr_map]
simp only [Multiset.quot_mk_to_coe'', Multiset.coe_eq_coe] at hl
exact hl.symm.pairwise hd fun h ↦ _root_.Disjoint.symm h
