re_ofReal — Mathlib

English

If a function f: C → C is analytic at a point x ∈ a complex normed space, then its real part, when restricted to the real axis, is analytic at x along the real parameter.

Русский

Если функция f: ℂ → ℂ аналитична в точке x ∈ ℂ, то её действительная часть, ограниченная к действительной оси, аналитична в x по вещественным переменным.

LaTeX

$$$\text{If } f:\mathbb{C}\to\mathbb{C} \text{ is analytic at } z_0\in\mathbb{C}, \text{ then the map } t\mapsto \operatorname{Re}(f(t)) \text{ is analytic at } t_0=\operatorname{Re}(z_0).$$$

Lean4

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

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