continuousAt — Mathlib

English

If f has a power series expansion p around x, then f is continuous at x. In particular, HasFPowerSeriesAt f p x implies ContinuousAt f x.

Русский

Если у функции f имеется степенной ряд вокруг точки x, то f непрерывна в точке x. В частности HasFPowerSeriesAt f p x ⇒ ContinuousAt f x.

LaTeX

$$$ HasFPowerSeriesAt f p x \Rightarrow ContinuousAt f x $$$

Lean4

protected theorem continuousAt (hf : HasFPowerSeriesAt f p x) : ContinuousAt f x :=
  let ⟨_, hr⟩ := hf
  hr.continuousOn.continuousAt (EMetric.ball_mem_nhds x hr.r_pos)

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