im_ofReal — Mathlib

English

If f is analytic on a punctured neighborhood image, then the imaginary part of f restricted to Real is analytic on that set.

Русский

Если f аналитична на образе окрестности без точки, то мнимая часть ограниченной Real аналитична на этом образе.

LaTeX

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

Lean4

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

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