sum — Mathlib

English

If each f i is L-series summable at s for i in S, then the sum over i∈S of f i is L-series summable at s.

Русский

Если каждый f i суммируем по L-рядy на s, тогда сумма по i∈S f i суммируема по L-рядy на s.

LaTeX

$$$\forall i:\, i\in S \Rightarrow LSeriesSummable (f i) s,\ LSeriesSummable (S\!\sum i=> f i) s$$$

Lean4

theorem sum (hf : ∀ i ∈ S, LSeriesSummable (f i) s) : LSeriesSummable (∑ i ∈ S, f i) s := by
  simpa [LSeriesSummable, ← term_sum_apply] using summable_sum hf

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