Theorems · Theorem · complex analysis

AnalyticOnNhd.eq_const_of_re_eq_const

∀ {f : ℂ → ℂ} {U : Set ℂ} {c₀ : ℝ},
  AnalyticOnNhd ℂ f U → (∀ x ∈ U, (f x).re = c₀) → IsOpen U → IsConnected U → ∃ c, ∀ x ∈ U, f x = c

Corollary to the open mapping theorem: A holomorphic function whose real part is constant is itself constant.

Defined in

Mathlib.Analysis.Complex.OpenMapping

Cited by

1 results in Mathlib

Foundations

Depth 298 from the axioms · uses propext, Classical.choice, Quot.sound