tendsto_trunc_atTop — Mathlib

English

The truncations of a power series converge to the series itself in the Pi-topology.

Русский

Усечения степенного ряда сходятся в сам ряд в Pi-топологии.

LaTeX

$$$ \\text{Tendsto}(d \\mapsto (\\operatorname{trunc}(d, f))) \\_{\\text{atTop}} \\to f $$$

Lean4

theorem tendsto_trunc_atTop [CommSemiring R] (f : R⟦X⟧) : Tendsto (fun d ↦ (trunc d f : R⟦X⟧)) atTop (𝓝 f) :=
  by
  rw [tendsto_iff_coeff_tendsto]
  intro d
  exact tendsto_atTop_of_eventually_const fun n (hdn : d < n) ↦ (by simp [coeff_trunc, hdn])

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