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:

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

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:

theorem List.support_sum_subset {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [AddMonoid M] (l : List (ι →₀ M)) :

(List.sum l).support ⊆ List.foldr (fun (x : ι →₀ M) (x_1 : Finset ι) => x.support ⊔ x_1) ∅ l

(Finset.sum s id).support ⊆ Finset.sup s Finsupp.support

theorem List.mem_foldr_sup_support_iff {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [Zero M] {l : List (ι →₀ M)} {x : ι} :

x ∈ List.foldr (fun (x : ι →₀ M) (x_1 : Finset ι) => x.support ⊔ x_1) ∅ 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 ∈ Multiset.sup (Multiset.map Finsupp.support s) ↔ ∃ 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 ∈ Finset.sup s Finsupp.support ↔ ∃ f ∈ s, x ∈ f.support

theorem List.support_sum_eq {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [AddMonoid M] (l : List (ι →₀ M)) (hl : List.Pairwise (Disjoint on Finsupp.support) l) :

(List.sum l).support = List.foldr (fun (x : ι →₀ M) (x_1 : Finset ι) => x.support ⊔ x_1) ∅ l

theorem Multiset.support_sum_eq {ι : Type u_1} {M : Type u_2} [DecidableEq ι] [AddCommMonoid M] (s : Multiset (ι →₀ M)) (hs : Multiset.Pairwise (Disjoint on Finsupp.support) s) :

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

(Finset.sum s id).support = Finset.sup s Finsupp.support

Documentation