hasSum_iff_hasSum_coeff — Mathlib

English

HasSum f g holds iff for every d, HasSum (i ↦ coeff_d(f_i)) (coeff_d(g)).

Русский

HasSum f g эквивалентно тому, что для каждого d выполнено HasSum (i ↦ coeff_d(f_i)) (coeff_d(g)).

LaTeX

$$$ HasSum f g \\iff \\forall d, HasSum (\\lambda i, coeff_d(f(i))) (coeff_d(g)) $$$

Lean4

theorem hasSum_iff_hasSum_coeff {g : R⟦X⟧} : HasSum f g ↔ ∀ d, HasSum (fun i ↦ coeff d (f i)) (coeff d g) :=
  by
  simp_rw [HasSum, ← map_sum]
  apply tendsto_iff_coeff_tendsto

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