analyticAt

Mathlib.Analysis.Analytic.CPolynomialDef

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

English

A CPolynomialAt function is analytic on the same domain set.

Русский

Функция CPolynomialAt аналитична на той же области определения.

LaTeX

$$CPolynomialAt 𝕜 f s → AnalyticOn 𝕜 f s$$

Lean4

theorem analyticAt (hf : CPolynomialAt 𝕜 f x) : AnalyticAt 𝕜 f x :=
  let ⟨p, _, hp⟩ := hf
  ⟨p, hp.hasFPowerSeriesAt⟩

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

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

Разделы

Аффилиация

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