mathlib documentation

data.finsupp.big_operators

Sums of collections of finsupp, and their support #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 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 : ι} :
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