analyticAt

Mathlib.Analysis.Analytic.Basic

URI: https://scilib.ai/kg/mathlib#HasFPowerSeriesAt.analyticAt

English

From HasFPowerSeriesWithinAt we deduce AnalyticAt by taking the same p and the center x.

Русский

Из HasFPowerSeriesWithinAt следует AnalyticAt, взяв тот же p и центр x.

LaTeX

$$$ HasFPowerSeriesWithinAt f p s x \Rightarrow AnalyticAt 𝕜 f x $$$

Lean4

theorem analyticAt (hf : HasFPowerSeriesAt f p x) : AnalyticAt 𝕜 f x :=
  ⟨p, hf⟩

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

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

Разделы

Аффилиация

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