# mathlib3documentation

data.finsupp.big_operators

# Sums of collections of finsupp, and their support #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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} [decidable_eq ι] [add_monoid M] (l : list →₀ M)) :
theorem multiset.support_sum_subset {ι : Type u_1} {M : Type u_2} [decidable_eq ι] (s : multiset →₀ M)) :
theorem finset.support_sum_subset {ι : Type u_1} {M : Type u_2} [decidable_eq ι] (s : finset →₀ M)) :
theorem list.mem_foldr_sup_support_iff {ι : Type u_1} {M : Type u_2} [decidable_eq ι] [has_zero M] {l : list →₀ M)} {x : ι} :
(f : ι →₀ M) (hf : f l), x f.support
theorem multiset.mem_sup_map_support_iff {ι : Type u_1} {M : Type u_2} [decidable_eq ι] [has_zero M] {s : multiset →₀ M)} {x : ι} :
(f : ι →₀ M) (hf : f s), x f.support
theorem finset.mem_sup_support_iff {ι : Type u_1} {M : Type u_2} [decidable_eq ι] [has_zero M] {s : finset →₀ M)} {x : ι} :
(f : ι →₀ M) (hf : f s), x f.support
theorem list.support_sum_eq {ι : Type u_1} {M : Type u_2} [decidable_eq ι] [add_monoid M] (l : list →₀ M)) (hl : l) :
theorem multiset.support_sum_eq {ι : Type u_1} {M : Type u_2} [decidable_eq ι] (s : multiset →₀ M)) (hs : s) :
theorem finset.support_sum_eq {ι : Type u_1} {M : Type u_2} [decidable_eq ι] (s : finset →₀ M))  :