analyticAt

Mathlib.Analysis.Analytic.CPolynomial

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

English

The analytic nature of a continuous multilinear map at a point x follows from its finite power-series expansion.

Русский

Аналитичность непрерывного многолинейного отображения в точке x вытекает из конечного разложения по степенным сериям.

LaTeX

$$AnalyticAt 𝕜 f x$$

Lean4

theorem analyticAt : AnalyticAt 𝕜 f x :=
  f.cpolynomialAt.analyticAt

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

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

Разделы

Аффилиация

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