# Documentation

Mathlib.Data.Finsupp.BigOperators

# Sums of collections of Finsupp, and their support #

This file provides results about the Finsupp.support of sums of collections of Finsupp, including sums of List, Multiset, and Finset.

The support of the sum is a subset of the union of the supports:

• List.support_sum_subset
• Multiset.support_sum_subset
• Finset.support_sum_subset

The support of the sum of pairwise disjoint finsupps is equal to the union of the supports

• List.support_sum_eq
• Multiset.support_sum_eq
• Finset.support_sum_eq

Member in the support of the indexed union over a collection iff it is a member of the support of a member of the collection:

• List.mem_foldr_sup_support_iff
• Multiset.mem_sup_map_support_iff
• Finset.mem_sup_support_iff
theorem List.support_sum_subset {ι : Type u_1} {M : Type u_2} [] [] (l : List (ι →₀ M)) :
().support List.foldr ((fun x x_1 => x x_1) Finsupp.support) l
theorem Multiset.support_sum_subset {ι : Type u_1} {M : Type u_2} [] [] (s : Multiset (ι →₀ M)) :
().support Multiset.sup (Multiset.map Finsupp.support s)
theorem Finset.support_sum_subset {ι : Type u_1} {M : Type u_2} [] [] (s : Finset (ι →₀ M)) :
(Finset.sum s id).support Finset.sup s Finsupp.support
theorem List.mem_foldr_sup_support_iff {ι : Type u_1} {M : Type u_2} [] [Zero M] {l : List (ι →₀ M)} {x : ι} :
x List.foldr ((fun x x_1 => x x_1) Finsupp.support) l f x, x f.support
theorem Multiset.mem_sup_map_support_iff {ι : Type u_1} {M : Type u_2} [] [Zero M] {s : Multiset (ι →₀ M)} {x : ι} :
x Multiset.sup (Multiset.map Finsupp.support s) f x, x f.support
theorem Finset.mem_sup_support_iff {ι : Type u_1} {M : Type u_2} [] [Zero M] {s : Finset (ι →₀ M)} {x : ι} :
x Finset.sup s Finsupp.support f x, x f.support
theorem List.support_sum_eq {ι : Type u_1} {M : Type u_2} [] [] (l : List (ι →₀ M)) (hl : List.Pairwise (Disjoint on Finsupp.support) l) :
().support = List.foldr ((fun x x_1 => x x_1) Finsupp.support) l
theorem Multiset.support_sum_eq {ι : Type u_1} {M : Type u_2} [] [] (s : Multiset (ι →₀ M)) (hs : Multiset.Pairwise (Disjoint on Finsupp.support) s) :
().support = Multiset.sup (Multiset.map Finsupp.support s)
theorem Finset.support_sum_eq {ι : Type u_1} {M : Type u_2} [] [] (s : Finset (ι →₀ M)) (hs : Set.PairwiseDisjoint (s) Finsupp.support) :
(Finset.sum s id).support = Finset.sup s Finsupp.support