isOpen_cpolynomialAt — Mathlib

English

If a function is CPolynomialAt at x, there exists a set s in the neighborhood of x on which the function is polynomial.

Русский

Если функция является CPolynomialAt в точке x, существует множество s в окрестности x, на котором функция полином.

LaTeX

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

Lean4

/-- For any function `f` from a normed vector space to a normed vector space, the set of points
`x` such that `f` is continuously polynomial at `x` is open. -/
theorem isOpen_cpolynomialAt : IsOpen {x | CPolynomialAt 𝕜 f x} :=
  by
  rw [isOpen_iff_mem_nhds]
  rintro x ⟨p, n, r, hr⟩
  exact mem_of_superset (EMetric.ball_mem_nhds _ hr.r_pos) fun y hy => hr.cpolynomialAt_of_mem hy

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