Theorems · Theorem · complex analysis

Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ},
  (∀ᶠ (z : ℂ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℂ f z) →
    ((fun z => f z - f c) =o[nhdsWithin c {c}ᶜ] fun z => (z - c)⁻¹) →
      Filter.Tendsto f (nhdsWithin c {c}ᶜ) (nhds ((nhdsWithin c {c}ᶜ).limUnder f))

Removable singularity theorem: if a function f : ℂ → E is complex differentiable on a punctured neighborhood of c and $f(z) - f(c)=o((z-c)^{-1})$, then f has a limit at c.

Defined in

Mathlib.Analysis.Complex.RemovableSingularity

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace