analyticOnNhd

Mathlib.Analysis.Analytic.CPolynomialDef

URI: https://scilib.ai/kg/mathlib#CPolynomialOn.analyticOnNhd

English

The statement that CPolynomialOn implies AnalyticOn.

Русский

Утверждение, что CPolynomialOn подразумевает AnalyticOn.

LaTeX

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

Lean4

theorem analyticOnNhd {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOnNhd 𝕜 f s := fun x hx ↦ (hf x hx).analyticAt

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

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

Разделы

Аффилиация

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