finsetSum_mem — Mathlib

English

If each f(x) ∈ I for x in a finite set, then the finite sum lies in I.

Русский

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

LaTeX

$$∀ x ∈ s, f x ∈ I ⇒ s.sum f ∈ I$$

Lean4

theorem finsetSum_mem {ι : Type*} (s : Finset ι) (f : ι → R) (hs : ∀ x ∈ s, f x ∈ I) : s.sum f ∈ I :=
  by
  rw [mem_iff, ← Finset.sum_const_zero]
  exact I.ringCon.finsetSum s hs

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