re_ofReal — Mathlib

English

If f is analytic on a punctured neighborhood image, then the real-part function is analytic on the base set.

Русский

Если f аналитична на образе окрестности без точки, то функция реальной части аналитична на базе.

LaTeX

$$$\\text{AnalyticOnNhd}_\\mathbb{R}(\\operatorname{Re}\\circ f)(s).$$$

Lean4

theorem re_ofReal (hf : AnalyticOnNhd ℂ f (ofReal '' s)) : AnalyticOnNhd ℝ (fun x : ℝ ↦ (f x).re) s :=
  ((Complex.reCLM.analyticOnNhd _).comp hf.restrictScalars (mapsTo_image f _)).comp (Complex.ofRealCLM.analyticOnNhd _)
    (mapsTo_image ofReal s)

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