analyticWithinAt

Mathlib.Analysis.Analytic.CPolynomial

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

English

Analyticity holds within a neighborhood of x for continuous multilinear maps.

Русский

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

LaTeX

$$AnalyticWithinAt 𝕜 f s x$$

Lean4

theorem analyticWithinAt : AnalyticWithinAt 𝕜 f s x :=
  f.analyticAt.analyticWithinAt

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

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

Разделы

Аффилиация

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