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)) :
l.sum.support ⊆ list.foldr (has_sup.sup ∘ finsupp.support) ∅ l
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
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 : ι} :
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
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
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) :