English
If f is analytic at x, then there exists a neighborhood of x such that f is continuous at all points y in that neighborhood, i.e., eventually, ContinuousAt f y along nhds x.
Русский
Если функция аналитична в точке x, то существует окрестность x, внутри которой f непрерывна в каждой точке; т.е. предел непрерывности достигается для почти всех y около x.
LaTeX
$$$ AnalyticAt 𝕜 f x \Rightarrow \forall \; \text{nhds } x, \; \text{(f is continuous nearby)} $$$
Lean4
protected theorem eventually_continuousAt (hf : AnalyticAt 𝕜 f x) : ∀ᶠ y in 𝓝 x, ContinuousAt f y :=
by
rcases hf with ⟨g, r, hg⟩
have : EMetric.ball x r ∈ 𝓝 x := EMetric.ball_mem_nhds _ hg.r_pos
filter_upwards [this] with y hy
apply hg.continuousOn.continuousAt
exact EMetric.isOpen_ball.mem_nhds hy
