Theorems · Theorem · complex analysis

HasStrictDerivAt.real_of_complex

∀ {e : ℂ → ℂ} {e' : ℂ} {z : ℝ}, HasStrictDerivAt e e' ↑z → HasStrictDerivAt (fun x => (e ↑x).re) e'.re z

If a complex function is differentiable at a real point, then the induced real function is also differentiable at this point, with a derivative equal to the real part of the complex derivative.

Defined in

Mathlib.Analysis.Complex.RealDeriv

Cited by

6 results in Mathlib

Foundations

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