continuousAt

Mathlib.Analysis.Analytic.CPolynomialDef

URI: https://scilib.ai/kg/mathlib#HasFiniteFPowerSeriesAt.continuousAt

English

If f has a finite power series, then f is continuous at x.

Русский

Если у f есть конечный степенной ряд, то f непрерывна в точке x.

LaTeX

$$HasFiniteFPowerSeriesOnBall f p x n → ContinuousAt f x$$

Lean4

protected theorem continuousAt (hf : HasFiniteFPowerSeriesAt f p x n) : ContinuousAt f x :=
  hf.hasFPowerSeriesAt.continuousAt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru