eventually_cpolynomialAt — Mathlib

English

If f is continuously polynomial at x, then there exists a ball around x where f remains continuously polynomial.

Русский

Если f непрерывно полином в точке x, то существует шар вокруг x, где f остаётся непрерывно полином.

LaTeX

$$∃ r>0, CPolynomialOn 𝕜 f (Metric.ball x r)$$

Lean4

theorem eventually_cpolynomialAt {f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) : ∀ᶠ y in 𝓝 x, CPolynomialAt 𝕜 f y :=
  (isOpen_cpolynomialAt 𝕜 f).mem_nhds h

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