mathlib documentation

data.finsupp.big_operators

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} [decidable_eq ι] [add_monoid M] (l : list →₀ M)) :
theorem multiset.support_sum_subset {ι : Type u_1} {M : Type u_2} [decidable_eq ι] [add_comm_monoid M] (s : multiset →₀ M)) :
theorem finset.support_sum_subset {ι : Type u_1} {M : Type u_2} [decidable_eq ι] [add_comm_monoid M] (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 : ι} :
x list.foldr (has_sup.sup finsupp.support) l ∃ (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 : ι} :
x (multiset.map finsupp.support s).sup ∃ (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 : ι} :
x s.sup finsupp.support ∃ (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 : list.pairwise (disjoint on finsupp.support) l) :
theorem finset.support_sum_eq {ι : Type u_1} {M : Type u_2} [decidable_eq ι] [add_comm_monoid M] (s : finset →₀ M)) (hs : s.pairwise_disjoint finsupp.support) :