tendsto_iff_coeff_tendsto — Mathlib

English

Tendsto f u (nhds g) holds if and only if each coefficient map tends to the corresponding coefficient of g.

Русский

Сходимость f по u к nhds g эквивалентна сходимости каждой координатной карты коэффициентов к соответствующему коэффициенту g.

LaTeX

$$Tendsto f u (nhds g) ↔ ∀ d, Tendsto (λ i, coeff d (f i)) u (nhds (coeff d g))$$

Lean4

/-- A family of power series converges iff it converges coefficientwise -/
theorem tendsto_iff_coeff_tendsto [Semiring R] {ι : Type*} (f : ι → MvPowerSeries σ R) (u : Filter ι)
    (g : MvPowerSeries σ R) :
    Tendsto f u (nhds g) ↔ ∀ d : σ →₀ ℕ, Tendsto (fun i => coeff d (f i)) u (nhds (coeff d g)) :=
  by
  rw [nhds_pi, tendsto_pi]
  exact forall_congr' (fun d => Iff.rfl)

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