sum_mem — Mathlib

English

If each f(i) ∈ p for i in a finite set t, then the finite sum ∑ f(i) belongs to p.

Русский

Если для всех i в конечном множество t выполняется f(i) ∈ p, то сумма ∑ f(i) принадлежит p.

LaTeX

$${\exists t, f : ι → M, (∀ i ∈ t, f(i) ∈ p) → (∑ i ∈ t, f(i)) ∈ p}$$

Lean4

protected theorem sum_mem {t : Finset ι} {f : ι → M} : (∀ c ∈ t, f c ∈ p) → (∑ i ∈ t, f i) ∈ p :=
  sum_mem

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