English
If a complex function e is differentiable at a real point, then the real-valued function x ↦ Re(e(x)) is differentiable there with derivative equal to Re(e').
Русский
Если комплексная функция e дифференцируема в действительной точке, то функция x ↦ Re(e(x)) дифференцируема там с производной равной Re(e').
LaTeX
$$$\displaystyle \text{If } e: \mathbb{C} \to \mathbb{C} \text{ is differentiable at } z \text{ with derivative } e', \text{ then } x \mapsto \Re(e(x)) \text{ has derivative } \Re(e') \text{ at } z.$$$
Lean4
/-- If a function `f : ℝ → ℝ` is differentiable at a (real) point `x`, then it is also
differentiable as a function `ℝ → ℂ`. -/
theorem ofReal_comp {f : ℝ → ℝ} {u : ℝ} (hf : HasDerivAt f u z) : HasDerivAt (fun y : ℝ => ↑(f y) : ℝ → ℂ) u z := by
simpa only [ofRealCLM_apply, ofReal_one, real_smul, mul_one] using ofRealCLM.hasDerivAt.scomp z hf
