English
If f is analytic withinAt at x, there exists a neighborhood u ∈ 𝓝[insert x s] x such that f is analytic on u.
Русский
Если f аналитична внутри в точке x, существует окрестность u ∈ 𝓝[insert x s] x такая, что f аналитична на u.
LaTeX
$$$AnalyticWithinAt 𝕜 f s x \Rightarrow \exists u \in 𝓝[insert x s] x, AnalyticOn 𝕜 f u$$$
Lean4
theorem exists_mem_nhdsWithin_analyticOn [CompleteSpace F] {f : E → F} {s : Set E} {x : E}
(h : AnalyticWithinAt 𝕜 f s x) : ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u :=
by
obtain ⟨g, -, h'g, hg⟩ : ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x := h.exists_analyticAt
let u := insert x s ∩ {y | AnalyticAt 𝕜 g y}
refine ⟨u, ?_, ?_⟩
· exact inter_mem_nhdsWithin _ ((isOpen_analyticAt 𝕜 g).mem_nhds hg)
· intro y hy
have : AnalyticWithinAt 𝕜 g u y := hy.2.analyticWithinAt
exact this.congr (h'g.mono (inter_subset_left)) (h'g (inter_subset_left hy))
