exists_mem_nhds_cpolynomialOn

Mathlib.Analysis.Analytic.CPolynomialDef

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

← MathLib Explorer

English

If f is CPolynomialAt x, there exists s in nhds x such that CPolynomialOn 𝕜 f s.

Русский

Если f = CPolynomialAt в x, существует s ∈ nhds x, такое что CPolynomialOn 𝕜 f s.

LaTeX

$$∃ s ∈ 𝓝 x, CPolynomialOn 𝕜 f s$$

Lean4

theorem exists_mem_nhds_cpolynomialOn {f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) : ∃ s ∈ 𝓝 x, CPolynomialOn 𝕜 f s :=
  h.eventually_cpolynomialAt.exists_mem

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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