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:

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 (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 (Multiset.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 List.foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) => x1.support x2) l fl, 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 fs, 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 fs, 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 (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 : 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