Theorems · Theorem · complex analysis

Complex.norm_cderiv_sub_lt

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {z : ℂ} {M r : ℝ} {f g : ℂ → E},
  0 < r →
    (∀ w ∈ Metric.sphere z r, ‖f w - g w‖ < M) →
      ContinuousOn f (Metric.sphere z r) →
        ContinuousOn g (Metric.sphere z r) → ‖Complex.cderiv r f z - Complex.cderiv r g z‖ < M / r

Defined in

Mathlib.Analysis.Complex.LocallyUniformLimit

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace