real_of_complex — Mathlib

English

If e: ℂ → ℂ is ContDiff of order n, then the real-valued map x ↦ Re(e(Complex.ofReal x)) is ContDiff of order n on ℝ.

Русский

Если e: ℂ → ℂ имеет континуальную дифференцируемость порядка n, то функция x ↦ Re(e(Complex.ofReal x)) на ℝ также имеет порядок n континуированной дифференцируемости.

LaTeX

$$$\displaystyle \text{If } e: \mathbb{C} \to \mathbb{C} \text{ is ContDiff }_\mathbb{C}^n, \text{ then } x \mapsto \Re(e(\mathrm{Complex.ofReal}(x))) \text{ is ContDiff }_\mathbb{R}^n.$$$

Lean4

theorem real_of_complex {n : WithTop ℕ∞} (h : ContDiff ℂ n e) : ContDiff ℝ n fun x : ℝ => (e x).re :=
  contDiff_iff_contDiffAt.2 fun _ => h.contDiffAt.real_of_complex

Похожие утверждения