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:

source

theorem list.support_sum_subset {ι : Type u_1} {M : Type u_2} [decidable_eq ι] [add_monoid M] (l : list (ι →₀ M)) :

l.sum.support ⊆ list.foldr (has_sup.sup ∘ finsupp.support) ∅ l

source

theorem multiset.support_sum_subset {ι : Type u_1} {M : Type u_2} [decidable_eq ι] [add_comm_monoid M] (s : multiset (ι →₀ M)) :

s.sum.support ⊆ (multiset.map finsupp.support s).sup

source

theorem finset.support_sum_subset {ι : Type u_1} {M : Type u_2} [decidable_eq ι] [add_comm_monoid M] (s : finset (ι →₀ M)) :

(s.sum id).support ⊆ s.sup finsupp.support

source

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

source

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

source

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

source

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

l.sum.support = list.foldr (has_sup.sup ∘ finsupp.support) ∅ l

source

theorem multiset.support_sum_eq {ι : Type u_1} {M : Type u_2} [decidable_eq ι] [add_comm_monoid M] (s : multiset (ι →₀ M)) (hs : multiset.pairwise (disjoint on finsupp.support) s) :

s.sum.support = (multiset.map finsupp.support s).sup

source

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

(s.sum id).support = s.sup finsupp.support