support_sum_subset — Mathlib

English

Analogous to lists, the sum of a multiset of finsupps has support contained in the supremum of mapped supports.

Русский

Аналогично спискам, сумма мультимножества финспп имеет опору внутри супремума приведённых опор.

LaTeX

$$$\\operatorname{supp}(\\\\operatorname{sum} s) \\\\subseteq (\\\\operatorname{map}\\\\ Finsupp.\\\\operatorname{support} s) \\\\mathsf{sup}$$$

Lean4

theorem support_sum_subset [AddCommMonoid M] (s : Multiset (ι →₀ M)) : s.sum.support ⊆ (s.map Finsupp.support).sup :=
  by
  induction s using Quot.inductionOn
  simpa only [Multiset.quot_mk_to_coe'', Multiset.sum_coe, Multiset.map_coe, Multiset.sup_coe, List.foldr_map] using
    List.support_sum_subset _

Похожие утверждения