multisetSum_mem — Mathlib

English

If each mapped element is in I, then the multiset sum is in I.

Русский

Если каждый отображённый элемент принадлежит I, то сумма по множеству в I.

LaTeX

$$∀ x ∈ s, f x ∈ I ⇒ (s.map f).sum ∈ I$$

Lean4

theorem multisetSum_mem {ι : Type*} (s : Multiset ι) (f : ι → R) (hs : ∀ x ∈ s, f x ∈ I) : (s.map f).sum ∈ I :=
  by
  rw [mem_iff, ← Multiset.sum_map_zero]
  exact I.ringCon.multisetSum s hs

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