eventually_analyticAt — Mathlib

English

If a function f: E → F is analytic at a point x ∈ E, then there exists a neighborhood U of x such that f is analytic at every point y ∈ U.

Русский

Если функция f: E → F аналитична в точке x ∈ E, то существует окрестность U точки x, такая что для всякой y ∈ U функция f аналитична в y.

LaTeX

$$$\\exists U \\in \\mathcal{N}(x): \\forall y \\in U, \\text{AnalyticAt}_{\\mathbb{K}}(f,y).$$$

Lean4

theorem eventually_analyticAt (h : AnalyticAt 𝕜 f x) : ∀ᶠ y in 𝓝 x, AnalyticAt 𝕜 f y :=
  (isOpen_analyticAt 𝕜 f).mem_nhds h

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