Theorems · Theorem · complex analysis

Complex.differentiableOn_compl_singleton_and_continuousAt_iff

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ}
  {c : ℂ}, s ∈ nhds c → (DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c ↔ DifferentiableOn ℂ f s)

Defined in

Mathlib.Analysis.Complex.RemovableSingularity

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace