English
If a function f admits a formal power series expansion p around a point x, then there exists a neighborhood of zero (within positive radii) such that the expansion converges on balls B(x, r) for all small radii r.
Русский
Если функция f имеет формальную степенную серию p вокруг точки x, существует окрестность нуля (с положительным радиусом), такая что разложение сходится на шарах B(x, r) для всех малых радиусов r.
LaTeX
$$$\\text{HasFPowerSeriesAt } f p x \\Rightarrow \\forall^\\infty r \\in 𝓝[>] 0,\\ HasFPowerSeriesOnBall f p x r.$$$
Lean4
protected theorem eventually (hf : HasFPowerSeriesAt f p x) : ∀ᶠ r : ℝ≥0∞ in 𝓝[>] 0, HasFPowerSeriesOnBall f p x r :=
let ⟨_, hr⟩ := hf
mem_of_superset (Ioo_mem_nhdsGT hr.r_pos) fun _ hr' => hr.mono hr'.1 hr'.2.le
