English
For a finsupp Finset, the sum’s support equals the Finset supremum of the mapped supports provided pairwise disjointness holds.
Русский
Для финсет суммирование опор равно супремусу опор в отображаемом образе при условии попарной совместимости.
LaTeX
$$$\\operatorname{supportSumEq}$: $ (s.sum id).\\\\support = \\\\operatorname{sup} \\,s \\, Finsupp.\\\\operatorname{support} $$$
Lean4
theorem support_sum_eq [AddCommMonoid M] (s : Finset (ι →₀ M))
(hs : (s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support) : (s.sum id).support = Finset.sup s Finsupp.support := by
classical
suffices s.1.Pairwise (_root_.Disjoint on Finsupp.support)
by
convert Multiset.support_sum_eq s.1 this
exact (Finset.sum_val _).symm
obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup :=
by
refine ⟨s.toList, ?_, Finset.nodup_toList _⟩
simp
subst hl
rwa [List.toFinset_val, List.dedup_eq_self.mpr hn, Multiset.pairwise_coe_iff_pairwise, ←
List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn]
intro x y hxy
exact symmetric_disjoint hxy
