Theorems · Theorem · complex analysis

HasDerivAt.comp_ofReal

∀ {e : ℂ → ℂ} {e' : ℂ} {z : ℝ}, HasDerivAt e e' ↑z → HasDerivAt (fun y => e ↑y) e' z

If a complex function e is differentiable at a real point, then its restriction to ℝ is differentiable there as a function ℝ → ℂ, with the same derivative.

Defined in

Mathlib.Analysis.Complex.RealDeriv

Cited by

11 results in Mathlib

Foundations

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