hasFPowerSeriesWithinOnBall_univ — Mathlib

English

Near x, HasFPowerSeriesOnBall yields HasSum with y−x around x.

Русский

В окрестности x степенной ряд даёт сумму с y−x вокруг x.

LaTeX

$$$HasFPowerSeriesOnBall\\; f\\; p\\; x\\; r \\Rightarrow \\\\forall^\\infty y \\in 𝓝 x,\\ HasSum(\\lambda n : \\mathbb{N}, p_n(\\lambda _ : Fin n => y - x))(f(y)).$$$

Lean4

@[simp]
theorem hasFPowerSeriesWithinOnBall_univ : HasFPowerSeriesWithinOnBall f p univ x r ↔ HasFPowerSeriesOnBall f p x r :=
  by
  constructor
  · intro h
    refine ⟨h.r_le, h.r_pos, fun {y} m ↦ h.hasSum (by simp) m⟩
  · intro h
    exact ⟨h.r_le, h.r_pos, fun {y} _ m => h.hasSum m⟩

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