listSum_mem — Mathlib

English

If every f(x) ∈ I for x in a list, then the sum of the mapped elements lies in I.

Русский

Если для каждого элемента x списка выполняется f(x) ∈ I, тогда сумма отображённых элементов лежит в I.

LaTeX

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

Lean4

theorem listSum_mem {ι : Type*} (l : List ι) (f : ι → R) (hl : ∀ x ∈ l, f x ∈ I) : (l.map f).sum ∈ I :=
  by
  rw [mem_iff, ← List.sum_map_zero]
  exact I.ringCon.listSum l hl

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