exists_mem_nhds_analyticOnNhd — Mathlib

English

If h asserts analyticity of f at x, then there exists a neighborhood s of x such that f is analytic on nhd s (i.e., analytic on a neighborhood determined by s).

Русский

Если функция f аналитична в точке x, тогда существует окрестность s точки x, такая что f аналитична на некоторой окрестности s.

LaTeX

$$$\\exists s \\in \\mathcal{N}(x),\\ AnalyticOnNhd_{\\mathbb{K}}(f,s).$$$

Lean4

theorem exists_mem_nhds_analyticOnNhd (h : AnalyticAt 𝕜 f x) : ∃ s ∈ 𝓝 x, AnalyticOnNhd 𝕜 f s :=
  h.eventually_analyticAt.exists_mem

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