Theorems · Theorem · complex analysis

Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ},
  (∀ᶠ (z : ℂ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℂ f z) → ContinuousAt f c → AnalyticAt ℂ f c

Removable singularity theorem, weak version. If f : ℂ → E is differentiable in a punctured neighborhood of a point and is continuous at this point, then it is analytic at this point.

Defined in

Mathlib.Analysis.Complex.RemovableSingularity

Cited by

1 results in Mathlib

Foundations

Depth 283 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace