im_ofReal — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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