Liouville's Theorem for Harmonic Functions on the Complex Plane

A bounded harmonic function on the complex plane is constant.

theorem InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℂ → E) (h_harm : HarmonicOnNhd f Set.univ) (h_bound : Bornology.IsBounded (Set.range f)) (z w : ℂ) : f z = f w

Liouville's theorem for harmonic functions on the complex plane A bounded harmonic function on the complex plane is constant.