analyticWithinAt

Mathlib.Analysis.Analytic.CPolynomialDef

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

English

From analyticOnNhd to analyticOn, CPolynomialOn yields local analyticity on sets.

Русский

Из analyticOnNhd в analyticOn, CPolynomialOn даёт локальную аналитичность на множествах.

LaTeX

$$CPolynomialOn 𝕜 f s → AnalyticOn 𝕜 f s$$

Lean4

theorem analyticWithinAt {s : Set E} (hf : CPolynomialAt 𝕜 f x) : AnalyticWithinAt 𝕜 f s x :=
  hf.analyticAt.analyticWithinAt

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

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

Разделы

Аффилиация

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