sum — Mathlib

English

If each f i has HasSum f i s a i for i in S, then the finitely summed f i has HasSum s with sum equal to the finitely summed a i.

Русский

Если для каждого i из S верно HasSum f i s a i, то S-сумма f i имеет HasSum s с суммой равной S-сумме a i.

LaTeX

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

Lean4

theorem sum {a : ι → ℂ} (hf : ∀ i ∈ S, LSeriesHasSum (f i) s (a i)) : LSeriesHasSum (∑ i ∈ S, f i) s (∑ i ∈ S, a i) :=
  by simpa [LSeriesHasSum, term_sum, Finset.sum_fn S fun i ↦ term (f i) s] using hasSum_sum hf

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