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} [DecidableEq ι] [AddZeroClass M] (l : List (ι →₀ M)) : l.sum.support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) => x1.support ⊔ x2) ∅ l

theorem Multiset.support_sum_subset {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [AddCommMonoid M] (s : Multiset (ι →₀ M)) : s.sum.support ⊆ (map Finsupp.support s).sup

theorem Finset.support_sum_subset {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [AddCommMonoid M] (s : Finset (ι →₀ M)) : (s.sum id).support ⊆ s.sup Finsupp.support

theorem List.mem_foldr_sup_support_iff {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [Zero M] {l : List (ι →₀ M)} {x : ι} : x ∈ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) => x1.support ⊔ x2) ∅ l ↔ ∃ f ∈ l, x ∈ f.support

theorem Multiset.mem_sup_map_support_iff {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [Zero M] {s : Multiset (ι →₀ M)} {x : ι} : x ∈ (map Finsupp.support s).sup ↔ ∃ f ∈ s, x ∈ f.support

theorem Finset.mem_sup_support_iff {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [Zero M] {s : Finset (ι →₀ M)} {x : ι} : x ∈ s.sup Finsupp.support ↔ ∃ f ∈ s, x ∈ f.support

theorem List.support_sum_eq {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [AddZeroClass M] (l : List (ι →₀ M)) (hl : Pairwise (Function.onFun _root_.Disjoint Finsupp.support) l) : l.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) => x1.support ⊔ x2) ∅ l

theorem Multiset.support_sum_eq {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [AddCommMonoid M] (s : Multiset (ι →₀ M)) (hs : Pairwise (Function.onFun Disjoint Finsupp.support) s) : s.sum.support = (map Finsupp.support s).sup

theorem Finset.support_sum_eq {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [AddCommMonoid M] (s : Finset (ι →₀ M)) (hs : (↑s).PairwiseDisjoint Finsupp.support) : (s.sum id).support = s.sup Finsupp.support