tendstoLocallyUniformlyOn' — Mathlib

English

Continuity is inherited: if a function has a power-series within-ball, then it is continuous there.

Русский

Непрерывность сохраняется: если есть разложение в шаре, то функция непрерывна там.

LaTeX

$$$\text{continuousWithinOnBall}$$$

Lean4

/-- If a function admits a power series expansion at `x`, then it is the locally uniform limit of
the partial sums of this power series on the disk of convergence, i.e., `f y`
is the locally uniform limit of `p.partialSum n (y - x)` there. -/
theorem tendstoLocallyUniformlyOn' (hf : HasFPowerSeriesOnBall f p x r) :
    TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (EMetric.ball (x : E) r) :=
  by
  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
  simpa using hf.tendstoLocallyUniformlyOn'

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