harmonic_is_realOfHolomorphic

Deprecated since 2026-03-03Use InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq instead.

∀ {f : ℂ → ℝ} {z : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicOnNhd f (Metric.ball z R) →
    ∃ F, AnalyticOnNhd ℂ F (Metric.ball z R) ∧ Set.EqOn (fun z => (F z).re) f (Metric.ball z R)

Alias of InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq.

Defined in: Mathlib.Analysis.Complex.Harmonic.Analytic
Cited by: 0 results in Mathlib
Foundations: Depth 288 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement · cited by 25,697
Complexstatement · cited by 5,565
Complex.restatement · cited by 882
Metric.ballstatement · cited by 735
Set.EqOnstatement · cited by 603
AnalyticOnNhdstatement · cited by 206
InnerProductSpace.HarmonicOnNhdstatement · cited by 24
InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eqproof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.