English
If a function is differentiable on a set and that set is a neighborhood of z, then the function is analytic at z.
Русский
Если функция дифференцируема на некотором множестве и это множество содержит окрестность точки z, то функция аналитична в точке z.
LaTeX
$$AnalyticAt ℂ f z$$
Lean4
/-- If `f : ℂ → E` is complex differentiable on some set `s`, then it is analytic at any point `z`
such that `s ∈ 𝓝 z` (equivalently, `z ∈ interior s`). -/
protected theorem _root_.DifferentiableOn.analyticAt {s : Set ℂ} {f : ℂ → E} {z : ℂ} (hd : DifferentiableOn ℂ f s)
(hz : s ∈ 𝓝 z) : AnalyticAt ℂ f z :=
by
rcases nhds_basis_closedBall.mem_iff.1 hz with ⟨R, hR0, hRs⟩
lift R to ℝ≥0 using hR0.le
exact ((hd.mono hRs).hasFPowerSeriesOnBall hR0).analyticAt
