Theorems · Theorem · complex analysis

TendstoLocallyUniformlyOn.differentiableOn

∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {U : Set ℂ} {φ : Filter ι}
  {F : ι → ℂ → E} {f : ℂ → E} [CompleteSpace E] [φ.NeBot],
  TendstoLocallyUniformlyOn F f φ U → (∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U) → IsOpen U → DifferentiableOn ℂ f U

A locally uniform limit of holomorphic functions on an open domain of the complex plane is holomorphic (the derivatives converge locally uniformly to that of the limit, which is proved as TendstoLocallyUniformlyOn.deriv).

Defined in

Mathlib.Analysis.Complex.LocallyUniformLimit

Cited by

7 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceFilter.NeBot