hasFPowerSeriesAt

Mathlib.Analysis.Analytic.Basic

URI: https://scilib.ai/kg/mathlib#HasFPowerSeriesOnBall.hasFPowerSeriesAt

English

If a function has a power series on a ball, then it has a power series at a point.

Русский

Если функция имеет степенной ряд на шаре, значит, она имеет степенной ряд в точке.

LaTeX

$$$ HasFPowerSeriesOnBall f p x r \Rightarrow HasFPowerSeriesAt f p x $$$

Lean4

theorem hasFPowerSeriesAt (hf : HasFPowerSeriesOnBall f p x r) : HasFPowerSeriesAt f p x :=
  ⟨r, hf⟩

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

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

Разделы

Аффилиация

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