im_ofReal — Mathlib

English

If f is analytic within a set mapped from the real line, then the real-variable function t ↦ Im(f(t)) is analytic on that set.

Русский

Если f аналитична на внутри множества, полученного отображением из действительных, то функция t ↦ Im(f(t)) аналитична на этом множестве.

LaTeX

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

Lean4

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

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