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)) :

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

s.sum.support ⊆ (Multiset.map Finsupp.support s).sup

(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 ∈ 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.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 ι] [AddMonoid M] (l : List (ι →₀ M)) (hl : List.Pairwise (Disjoint on Finsupp.support) l) :

l.sum.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) :

s.sum.support = (Multiset.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

Documentation