TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A nonconstant scalar holomorphic function on a domain in $C^{m}$ is an open map

Statement

Let $m \geq 1$ , let $U \subseteq C^{m}$ be a nonempty connected open set, and let $f : U \to C$ be holomorphic and nonconstant. Then $f$ is an open map: for every open set $O \subseteq U$ , the image $f (O)$ is open in $C$ .

This theorem is about scalar-valued holomorphic functions. It asserts nothing for holomorphic maps into $C^{n}$ with $n \geq 2$ .

Facts & Assumptions

Given: A nonempty connected open set $U \subseteq C^{m}$ , a nonconstant holomorphic function $f : U \to C$ , and an open set $O \subseteq U$ .

[L1]

A holomorphic function vanishing on a nonempty open subset of a connected open set in $C^{m}$ vanishes identically (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

[L2]

The composite of holomorphic maps is holomorphic and its complex Jacobian is the product (The composite of holomorphic maps is holomorphic and its complex Jacobian is the product).

[L3]

Every nonconstant holomorphic function on a one-variable complex domain is an open map (Open mapping theorem for holomorphic functions).

[L4]

Balls in $C^{m}$ are the Euclidean balls of Balls, polydiscs and the distinguished boundary in $C^{m}$ , and convex subsets are those containing the segment between any two of their points (A convex subset of $R^{m}$ contains every line segment between two of its points).

[L5]

An open map sends open sets to open sets (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

Proof

technique · direct

1.1

Let $a \in O$ . Choose an open ball $B \subseteq O$ centred at $a$ . If $f$ were constant on $B$ , then $f - f (a)$ would vanish on the nonempty open set $B$ , and [L1] would force $f$ to be constant on all of $U$ , contrary to the hypothesis. So there is $b \in B$ with $f (b) \neq f (a)$ .

givenL1L4

2.1

Define $W : = {ξ \in C : a + ξ (b - a) \in B}$ . Because $B$ is convex, $W$ is a nonempty open disc about $0$ containing $1$ . The affine map $ℓ (ξ) : = a + ξ (b - a)$ is holomorphic, so [L2] makes $g : = f \circ ℓ$ holomorphic on $W$ ; and $g (0) = f (a) \neq f (b) = g (1)$ , so $g$ is nonconstant.

step 1.1L2L4

3.1

By [L3], the image $g (W)$ is open in $C$ and contains $g (0) = f (a)$ . Since $g (W) \subseteq f (B) \subseteq f (O)$ , the point $f (a)$ is interior to $f (O)$ . As $a \in O$ was arbitrary, every point of $f (O)$ is interior, so $f (O)$ is open by [L5]. Therefore $f$ is an open map.

step 2.1L3L5∎

Remarks

Why the theorem is scalar-valued. The proof restricts to a complex line and then invokes the one-variable open mapping theorem. That argument produces an open image only in $C$ , not for maps into higher-dimensional targets.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

M. Jabbari, Notes for Analysis and Geometry of Several Complex Variables, Thm. 22(9) (standard reference, not scraped)
J. Lebl, Tasty Bits of Several Complex Variables, v4.4, §1.2 (standard reference, not scraped)

A nonconstant scalar holomorphic function on a domain in CmCm is an open map