harmonicAt_re — Mathlib

English

If a complex-analytic function f: C → F is analytic, then its real part is harmonic at the same point.

Русский

Если функция f: C → F комплексно-аналитична, то её вещественная часть гармонична в той же точке.

LaTeX

$$$\text{If } h:\, \mathbb{C} \to F \text{ is analytic at } x,\ \operatorname{HarmonicAt}(\operatorname{Re}\circ f,x)$$$

Lean4

/-- If `f : ℂ → ℂ` is complex-analytic, then its real part is harmonic.
-/
theorem harmonicAt_re {f : ℂ → ℂ} (h : AnalyticAt ℂ f x) : HarmonicAt (fun z ↦ (f z).re) x :=
  h.harmonicAt.comp_CLM reCLM

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