hasSum_iff_hasSum_coeff — Mathlib

English

For a family f:ι → MvPowerSeries σ R and any g, HasSum f g holds if and only if for every coefficient index d, the family of scalars coeff d (f i) has sum coeff d g.

Русский

Для семейств f и g справедливо: HasSum f g тогда и только тогда, когда для каждого индекса коэффициентов d последовательность coeff d (f i) суммируема к coeff d g.

LaTeX

$$HasSum f g ↔ ∀ d : σ →₀ ℕ, HasSum (λ i, coeff d (f i)) (coeff d g)$$

Lean4

theorem hasSum_iff_hasSum_coeff {g : MvPowerSeries σ R} :
    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

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