eventually_eq_zero — Mathlib

English

If HasFPowerSeriesAt holds at x, then near x the HasSum with y near x holds for all y close to x.

Русский

Если существует степенной ряд в точке x, то при близких к x значениях y выполняется сумма ряда, дающая f(y).

LaTeX

$$$HasFPowerSeriesAt\\; f\\; p\\; x \\Rightarrow \\forall^\\infty y \\in 𝓝 x,\n HasSum\\left(\\lambda n. p_n(\\lambda _ : Fin n => y - x)\\right)(f(y)).$$$

Lean4

theorem eventually_eq_zero (hf : HasFPowerSeriesAt f (0 : FormalMultilinearSeries 𝕜 E F) x) : ∀ᶠ z in 𝓝 x, f z = 0 :=
  let ⟨_, hr⟩ := hf
  hr.eventually_eq_zero

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