English
If the point x belongs to the nhdsWithin x of s via the singleton {x}, then f is analytic within s at x. In other words, the local analyticity near x is automatic when x is 'isolated' inside s.
Русский
Если точка x принадлежит локальной окрестности nhdsWithin x через одиночку {x}, то функция f аналитична на области s в точке x. То есть локальная аналитичность в точке x следует автоматически, когда x является «изолированной» внутри s.
LaTeX
$$$\{x\} \in \mathcal{N}_s(x) \;\Rightarrow\; AnalyticWithinAt 𝕜 f s x$$$
Lean4
/-- `AnalyticWithinAt` is trivial if `{x} ∈ 𝓝[s] x` -/
theorem analyticWithinAt_of_singleton_mem {f : E → F} {s : Set E} {x : E} (h : { x } ∈ 𝓝[s] x) :
AnalyticWithinAt 𝕜 f s x := by
rcases mem_nhdsWithin.mp h with ⟨t, ot, xt, st⟩
rcases Metric.mem_nhds_iff.mp (ot.mem_nhds xt) with ⟨r, r0, rt⟩
exact
⟨constFormalMultilinearSeries 𝕜 E (f x), .ofReal r,
{ r_le := by simp only [FormalMultilinearSeries.constFormalMultilinearSeries_radius, le_top]
r_pos := by positivity
hasSum := by
intro y ys yr
simp only [subset_singleton_iff, mem_inter_iff, and_imp] at st
simp only [mem_insert_iff, add_eq_left] at ys
have : x + y = x := by
rcases ys with rfl | ys
· simp
· exact st (x + y) (rt (by simpa using yr)) ys
simp only [this]
apply (hasFPowerSeriesOnBall_const (e := 0)).hasSum
simp only [Metric.emetric_ball_top, mem_univ] }⟩
