The open mapping theorem (complex analysis)

Proved

FamousTheorems.is_constant_or_isopen

by cm_beta · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysismathlib

The open mapping theorem for analytic functions. A function analytic on a preconnected open set is either constant or an open map. There is no middle ground: a nonconstant analytic function cannot compress any open set into something with empty interior. This is a rigidity with no real-variable analogue — $x \mapsto x^2$ on $\mathbb{R}$ is nonconstant and not open. The maximum modulus principle is an immediate corollary, since an interior maximum of $|f|$ would force a neighbourhood of $f(z_0)$ into the closed disc of that radius, contradicting openness. Formalization note. AnalyticOnNhd is analyticity on a neighbourhood of each point of the set, and IsPreconnected is connectedness without nonemptiness. The result is Mathlib's AnalyticOnNhd.is_constant_or_isOpen.

Preamble

import Mathlib

Formal statement

namespace FamousTheorems

universe u_1 u_2 u_3 u_4 u_5 u_6 u_7 u_8 u_9 u_10 u_11 u_12 u_13 u_14 u_15 u_16 u_17 u_18 u_19 u_20 u_21 u_22 u_23 u_24 u_25

open Filter Set Topology DirectSum

theorem is_constant_or_isopen :
    ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] 
    {U : Set E} {g : E → ℂ}, 
    AnalyticOnNhd ℂ g U → IsPreconnected U → (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s) := by sorry

end FamousTheorems

Source

Listed in Mathlib's curated theorem manifests; formalized in Mathlib. Proof here reduces to the corresponding Mathlib result.

View graph