Complex analysis · existing Mathlib declaration

Holomorphic Open Mapping Theorem

An analytic map from a complex normed space into the complex plane has only two behaviors on a preconnected set: it is constant there, or it sends every ambient-open piece lying inside that set to an open region.

holomorphic functions
open mappings
preconnected sets
isolated zeros
maximum principle
complex-line restrictions

The theorem at a glance

Holomorphic Open Mapping Theorem at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

An ivory complex-analysis poster presents the exact constant-or-open alternative for an analytic map on a preconnected set, then traces isolated-zero separation, the maximum-principle target ball, a nonconstant complex-line direction, and propagation of local constancy. — Analyticity on a preconnected set forces constancy there or openness on every ambient-open piece contained in it.

Accessible poster text

Read the headline and panel text

COMPLEX ANALYSIS · HOLOMORPHIC MAPS

HOLOMORPHIC OPEN MAPPING THEOREM

g maps E into the complex plane

g analytic near every point of a preconnected set U

E a complex normed space

EITHER

g is constant on U

for every ambient-open s ⊆ U, g(s) is open in the complex plane

NONCONSTANT ANALYTIC MAPS OPEN THE AMBIENT-OPEN PIECES OF U

HOW THE SOURCE ROUTE MOVES

1 · Isolated zeros give a positive boundary minimum on a complex line

2 · The maximum principle puts a target ball inside the local image

3 · A nonconstant line direction gives local openness in E

4 · Preconnectedness propagates local constancy across U

EXACT SCOPE

U need not be open. No claim that g(U) is open unless U is open.

The detailed visual description covers the diagram and its local mathematical labels.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

A preconnected set U contains open pieces s₁ and s₂. A fork shows points collapsing to w in the constant branch, or the two pieces mapping to separate open regions f(s₁) and f(s₂). — Analyticity on a preconnected set forces constancy there or openness of the image of every ambient-open piece contained in it.

Complementary intuition

A mathematical landmark

The open mapping theorem is a central rigidity principle of complex analysis: nonconstant analytic behavior cannot flatten genuine neighborhoods. Mathlib's selected formulation exposes both the local analytic mechanism and its global propagation across a preconnected set, while allowing a higher-dimensional complex normed domain.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

theorem AnalyticOnNhd.is_constant_or_isOpen {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} {g : E → ℂ} (hg : AnalyticOnNhd ℂ g U) (hU : IsPreconnected U) : (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s)

Selected evidence declaration text

theorem AnalyticOnNhd.is_constant_or_isOpen {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} {g : E → ℂ} (hg : AnalyticOnNhd ℂ g U) (hU : IsPreconnected U) : (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s)

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Claim boundary

No new theorem is claimed

This page indexes Mathlib's global holomorphic open-mapping declaration for a map g from a complex normed space E to ℂ that is analytic on a neighborhood of every point of a preconnected set U. It proves a disjunction: either g is constant on U, or the image of every ambient-open subset s contained in U is open in ℂ. It does not require U to be open, assert that g(U) is open when U is not open, state a global IsOpenMap result, or allow an arbitrary vector-valued codomain.

The set U is assumed preconnected but need not be open; the selected declaration therefore does not conclude that g(U) is open unless U is open.
The open alternative ranges over ambient-open subsets s contained in U and is not itself a global IsOpenMap statement.
The domain may be an arbitrary complex normed space, but the codomain in the selected declaration is exactly ℂ rather than an arbitrary complex normed space.
The conclusion does not assert injectivity, conformality, biholomorphic inversion, or a quantitative distortion bound.
Proof Atlas is indexing an existing Mathlib theorem, and the generated explanation and visuals are not proof evidence.

Provenance

Origin and evidence stay separate

Existing declaration: AnalyticOnNhd.is_constant_or_isOpen in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.holomorphic-open-mapping-theorem.v001
Source handling: Verified upstream reference; no mirrored source package