im_ofReal — Mathlib

English

If a complex function f is analytic at a point x, then the imaginary part of f, viewed as a real-variable function, is analytic at x.

Русский

Если функция f комплексная аналитична в окрестности точки x, то мнимая часть f, как функция от реального аргумента, аналитична в точке x.

LaTeX

$$$\\text{AnalyticAt}_\\mathbb{R}(\\operatorname{Im}\\circ f)(x) \\text{ given } \\text{AnalyticAt}_\\mathbb{C} f(x).$$$

Lean4

@[fun_prop]
theorem im_ofReal (hf : AnalyticAt ℂ f x) : AnalyticAt ℝ (fun x : ℝ ↦ (f x).im) x :=
  (Complex.imCLM.analyticAt _).comp (hf.restrictScalars.comp (Complex.ofRealCLM.analyticAt _))

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