exists_ball_cpolynomialOn — Mathlib

English

If f is CPolynomialAt x, there exists a ball around x where f is CPolynomialOn.

Русский

Если f является CPolynomialAt в x, найдём шар вокруг x, на котором f является CPolynomialOn.

LaTeX

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

Lean4

/-- If `f` is continuously polynomial at a point, then it is continuously polynomial in a
nonempty ball around that point. -/
theorem exists_ball_cpolynomialOn {f : E → F} {x : E} (h : CPolynomialAt 𝕜 f x) :
    ∃ r : ℝ, 0 < r ∧ CPolynomialOn 𝕜 f (Metric.ball x r) :=
  Metric.isOpen_iff.mp (isOpen_cpolynomialAt _ _) _ h

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