toMultiset_sum — Mathlib

English

toMultiset respects finite sums: the image of a Finset sum equals the sum of the images.

Русский

toMultiset сохраняет конечные суммы: образ суммы равен сумме образов.

LaTeX

$$$$ toMultiset(\\sum i ∈ s, f i) = \\sum i ∈ s, toMultiset(f i). $$$$

Lean4

theorem toMultiset_sum {f : ι → α →₀ ℕ} (s : Finset ι) :
    Finsupp.toMultiset (∑ i ∈ s, f i) = ∑ i ∈ s, Finsupp.toMultiset (f i) :=
  map_sum Finsupp.toMultiset _ _

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