analyticAt — Mathlib

English

If f is differentiable on the complex plane, then it is continuously differentiable everywhere.

Русский

Если функция дифференцируема на всей плоскости, то она непрерывно дифференцируема везде.

LaTeX

$$ContDiff ℂ n f$$

Lean4

/-- A complex differentiable function `f : ℂ → E` is analytic at every point. -/
protected theorem _root_.Differentiable.analyticAt {f : ℂ → E} (hf : Differentiable ℂ f) (z : ℂ) : AnalyticAt ℂ f z :=
  hf.differentiableOn.analyticAt univ_mem

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