Alphabeta Math
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.

✓ 20 results · all verified · 18 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Identity Theorem, the Maximum Principle and the Open Mapping Theorem

1 · Prerequisites

2 · Summary

Holomorphic functions on a complex domain are analytic and therefore possess Taylor expansions, a well-defined order of vanishing, and local factorizations by their first nonzero Taylor term. The Cauchy theory on star-shaped domains supplies primitives, while the coordinate-plane dictionary connects complex derivatives to real total derivatives. Compactness and the extreme value theorem control continuous moduli on bounded closures.

Local factorization first yields the identity theorem and isolated zeros, then holomorphic logarithms and roots turn a nonconstant map into a power in a biholomorphic coordinate. This normal form gives local multiplicities and the open mapping theorem, from which maximum and minimum principles follow. Boundary and strip versions lead to Hadamard's three-lines theorem. Local degree also characterizes nonzero derivative and local invertibility, so injective holomorphic maps have holomorphic inverses on their open images.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Locally injective holomorphic maps

Definition

Let U⊆C be open, let f:U→C be holomorphic (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions), and let a∈U. The map f is locally injective at a if there is a neighbourhood V of a in U (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open) such that the restriction f∣V is injective (Injection, surjection, bijection). It is locally injective on U if it is locally injective at every point of U.

The neighbourhood may always be replaced by a smaller open disc centred at a, so this convention agrees with the usual disc formulation.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Biholomorphic maps between complex domains

Definition

Let U,V⊆C be complex domains (A complex domain is a nonempty connected open subset of C). A map f:U→V is biholomorphic if it is bijective (Injection, surjection, bijection), holomorphic, and its inverse f−1:V→U is holomorphic (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions). The map f is then a biholomorphism from U onto V.

For local use, a holomorphic map is biholomorphic between neighbourhoods of a and f(a) when it restricts to a biholomorphism between complex domains U′⊆U and V′⊆V contained in those neighbourhoods and satisfying a∈U′ and f(a)∈V′. The two membership conditions are what make the notion local at a: without them z↦z2 would qualify at 0 by restricting to a disc that avoids 0.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The locally zero locus of a holomorphic function is clopen

Statement

For a holomorphic function h on an open set U, the set of points having a neighbourhood on which h vanishes is both open and closed in U.

More precisely, put L(h):={a∈U: there is an open neighbourhood V⊆U of a such that h∣V=0}. Then L(h) and U∖L(h) are open in U (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

Facts & Assumptions

Given: An open set U⊆C, a holomorphic function h:U→C, and the locally zero locus L(h) defined above.

[L1]

If a holomorphic function has finite order m at b, then near b it has the form (z−b)mg(z) with g holomorphic and g(b)≠0; moreover, its order at b is +∞ exactly when it vanishes on a neighbourhood of b (The order of a zero is the exponent in its local holomorphic factorization).

[L2]

A function complex differentiable at a point is continuous at that point (Complex differentiability at a point implies continuity there).

Proof

technique · direct
1.1given

If a∈L(h), one of the neighbourhoods appearing in the definition of L(h) is contained in L(h), so L(h) is open in U; this also covers L(h)=∅.

1.2L1L2algebra

Let b∈U∖L(h). If h(b)≠0, [L2] gives a neighbourhood on which h is nonzero. If h(b)=0, then [L1] and b∉L(h) make the order finite, so h(z)=(z−b)mg(z) near b with g(b)≠0; after shrinking by [L2], g is nowhere zero there, and b is the only zero. In either case a neighbourhood of b contains no point of L(h), so U∖L(h) is open.

2.1step 1.1step 1.2∎

Thus L(h) is open and its complement in U is open, so L(h) is both open and closed in U.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Identity theorem for holomorphic functions

Statement

If two holomorphic functions on a complex domain agree on a set with an accumulation point in the domain, then they agree everywhere on the domain.

Precisely, let Ω⊆C be a complex domain (A complex domain is a nonempty connected open subset of C), let f,g:Ω→C be holomorphic, and suppose that some a∈Ω is an accumulation point of {z∈Ω:f(z)=g(z)}. Then f=g on Ω. The requirement a∈Ω is essential.

Facts & Assumptions

Given: A complex domain Ω, holomorphic functions f,g:Ω→C, an accumulation point a∈Ω of their agreement set, and the holomorphic difference h:=f−g supplied by Linearity, product, reciprocal, and quotient rules for complex derivatives. A nonempty subset of a connected space that is both open and closed is the whole space (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).

[L1]

For a holomorphic function h on an open set U, the set of points having a neighbourhood on which h vanishes is both open and closed in U (The locally zero locus of a holomorphic function is clopen).

[L2]

A holomorphic function has finite order m at a exactly when it factors near a as (z−a)mq(z) with q(a)≠0; its order is +∞ exactly when it vanishes on a neighbourhood of a (The order of a zero is the exponent in its local holomorphic factorization).

[L3]

If f:U→C is complex differentiable at a∈U, then f is continuous at a (Complex differentiability at a point implies continuity there).

Proof

technique · direct
1.1givenL2L3

The function h vanishes at points arbitrarily close to a. If it had finite order there, [L2] would give h(z)=(z−a)mq(z) with q(a)≠0, and [L3] would make q nonzero on a smaller neighbourhood; then h would have no zeros there other than possibly a, contrary to accumulation. Hence h has infinite order at a, so [L2] makes it vanish on a neighbourhood of a.

2.1step 1.1L1given

By [L1], the locally zero locus of h is open and closed in Ω; it is nonempty by step 1.1. Since Ω is connected, that locus is all of Ω.

3.1step 2.1∎

Therefore h(z)=0 for every z∈Ω, which means f(z)=g(z) throughout Ω.

Remarks

The accumulation point must belong to the domain. Accumulation only at a boundary point does not force identity, as the companion counterexample shows.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Zeros of a nonzero holomorphic function are isolated

Statement

A holomorphic function on a complex domain that is not identically zero has only isolated zeros.

That is, if f:Ω→C is holomorphic on a complex domain and f is not the zero function, then every a∈Ω with f(a)=0 has a neighbourhood in which a is the only zero of f.

Facts & Assumptions

Given: A complex domain Ω, a holomorphic function f:Ω→C that is not identically zero, and an arbitrary zero a∈Ω.

[L1]

If two holomorphic functions on a complex domain agree on a set with an accumulation point in the domain, then they agree everywhere on the domain (Identity theorem for holomorphic functions).

[L2]

A holomorphic function has finite order m at a exactly when it factors near a as (z−a)mg(z) with g(a)≠0; its order is +∞ exactly when it vanishes on a neighbourhood of a (The order of a zero is the exponent in its local holomorphic factorization).

[L3]

A complex differentiable function is continuous at the point of complex differentiability (Complex differentiability at a point implies continuity there).

Proof

technique · direct
1.1L1given

The function f cannot vanish on any neighbourhood of a, for otherwise its zero set would have the interior point a as an accumulation point and [L1], applied to f and the zero function, would make f identically zero on Ω.

2.1step 1.1L2L3

By step 1.1 and [L2], the order of f at a is finite, so f(z)=(z−a)mg(z) near a with g(a)≠0. By [L3], after shrinking the neighbourhood, g is nowhere zero there; since f(a)=0, the finite order m is positive, and a is the only zero of f in that neighbourhood.

3.1step 2.1∎

The zero a was arbitrary, so every zero of f is isolated; if f has no zeros, the conclusion is vacuous.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Local degree of a nonconstant holomorphic map

Definition

Let Ω be a complex domain, let f:Ω→C be nonconstant and holomorphic, and let a∈Ω. The local degree of f at a is deg⁡af:=ord⁡a(f−f(a)).

This is a positive natural number. Indeed, f−f(a) is not identically zero by Identity theorem for holomorphic functions, while it vanishes at a. Its zero at a is therefore isolated by Zeros of a nonzero holomorphic function are isolated, so it does not vanish on a neighbourhood of a. The equivalence in The order of a zero is the exponent in its local holomorphic factorization then rules out infinite order, and the convention of The order of a zero of a holomorphic function makes the remaining finite order positive. The local degree is also called the multiplicity of f at a.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The ring of holomorphic functions on a complex domain is an integral domain

Statement

The holomorphic functions on a complex domain form an integral domain under pointwise addition and multiplication.

More explicitly, for a complex domain Ω, the set H(Ω) of holomorphic functions Ω→C is a commutative subring of the function ring CΩ (The ring RX of all functions from a set X into a ring, with pointwise operations, Subring: a subset containing 1R and closed under addition, additive inverses and multiplication), its constant zero and one functions are distinct, and fg=0 implies f=0 or g=0 (Zero divisor, and integral domain: a commutative ring with 1≠0 and no zero divisors).

Facts & Assumptions

Given: A complex domain Ω (A complex domain is a nonempty connected open subset of C); the field C (C=R[x]/(x2+1) is a field, every element is uniquely a+bi, and every nonzero element has inverse (a−bi)/(a2+b2)); and the facts from Linearity, product, reciprocal, and quotient rules for complex derivatives that constants, sums, differences, and products of holomorphic functions are holomorphic, and that a holomorphic function nonzero at a point remains nonzero on some neighbourhood of that point.

[L1]

If two holomorphic functions on a complex domain agree on a set with an accumulation point in the domain, then they agree everywhere on the domain (Identity theorem for holomorphic functions).

[L2]

In a function ring the operations are pointwise, and its distinguished zero and one are the corresponding constant functions (The ring RX of all functions from a set X into a ring, with pointwise operations).

[L3]

An integral domain is a commutative ring with distinct zero and one and with no zero divisors (Zero divisor, and integral domain: a commutative ring with 1≠0 and no zero divisors).

Proof

technique · direct
1.1L2given

By the holomorphic algebra laws in the given facts, H(Ω) contains the constant functions and is closed under pointwise addition, subtraction, and multiplication; [L2] and the field laws therefore make it a commutative subring of CΩ.

1.2givenalgebra

Since Ω is nonempty and 0≠1 in C, the constant zero and one functions take different values at any point of Ω and are distinct.

1.3L1givenchoose

Suppose fg is the zero function and f is not the zero function. Choose a∈Ω with f(a)≠0. The given holomorphic algebra fact makes f nonzero on a neighbourhood of a, so g vanishes there; [L1] then makes g the zero function on Ω. Thus a zero product has a zero factor.

2.1step 1.1step 1.2step 1.3L3∎

Steps 1.1, 1.2, and 1.3 verify all clauses of [L3], so H(Ω) is an integral domain.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A nonvanishing holomorphic function on a disc has a holomorphic logarithm

Statement

If h is nowhere zero and holomorphic on a disc, then there is a holomorphic L on that disc with exp⁡L=h.

Precisely, if D(a,r) is an open disc with r>0 and h:D(a,r)→C is holomorphic and nowhere zero, then there is a holomorphic function L:D(a,r)→C satisfying exp⁡(L(z))=h(z) for every z∈D(a,r).

Facts & Assumptions

Given: A disc D(a,r) with r>0 and a nowhere-zero holomorphic function h on it. For z,w∈D(a,r) and t∈[0,1] the triangle inequality gives ∣((1−t)z+tw)−a∣≤(1−t)∣z−a∣+t∣w−a∣<r, so every segment between two points of the disc stays in it; taking z=a makes the disc star-shaped with respect to a in the sense of Complex star-shaped and convex domains are the published Euclidean notions under the identification C=R2 and Star-shaped open subsets of Euclidean space, and [L4] makes the disc a connected, hence a complex, domain. Also h′ is itself holomorphic on the disc, because a holomorphic function has complex derivatives of all orders locally (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle), so the quotient rule makes h′/h holomorphic there, h being nowhere zero (Linearity, product, reciprocal, and quotient rules for complex derivatives); and the complex chain rule, the derivative of exp⁡, and the exponential addition law are supplied by The chain rule for complex derivatives, The complex exponential is entire and its complex derivative is itself, and exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential.

[L1]

Every holomorphic function on an open set star-shaped with respect to a has a primitive there (Every holomorphic function on a star-shaped domain has a primitive).

[L2]

A holomorphic function whose derivative vanishes everywhere on a complex domain is constant (A holomorphic function with zero derivative on a domain is constant).

[L3]

For every nonzero complex number z, the solutions of exp⁡w=z are exactly Log⁡z+2πik with k∈Z (All logarithms of z≠0 are Log⁡z+2πik, k∈Z).

[L4]

A segment t↦(1−t)v0+tv1 that lies in a subset A is a continuous path in A, and a path-connected subset of a topological space is a connected subset (A finite concatenation of straight segments in Rn is a continuous path, Every path-connected space is connected, and every path component lies inside a component, claim 2).

Proof

technique · direct
1.1L1givenalgebra

By the star-shapedness in the Given and [L1], h′/h has a holomorphic primitive K on the disc. Put H(z):=K(z)−K(a); then H(a)=0 and H′=h′/h.

2.1step 1.1L2L4givenalgebra

The complex product and chain rules give (hexp⁡(−H))′=h′exp⁡(−H)−hH′exp⁡(−H)=0, so, the disc being a complex domain by [L4], [L2] makes hexp⁡(−H) constant; its value at a is h(a).

3.1step 2.1L3choose

Since h(a)≠0, choose by [L3] a complex number c with exp⁡c=h(a), and set L:=H+c.

4.1step 2.1step 3.1givenalgebra∎

The exponential addition law and step 2.1 give exp⁡L=exp⁡Hexp⁡c=exp⁡H h(a)=h throughout the disc, so L is the required holomorphic logarithm.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Holomorphic roots of a nonvanishing function on a disc

Statement

For every positive natural m, a nowhere-zero holomorphic function on a disc has a holomorphic mth root.

More precisely, if h is nowhere zero and holomorphic on D(a,r) and m∈N satisfies m≥1, then there is a holomorphic q on D(a,r) with qm=h. If ξm=h(a) is a prescribed scalar root, q may be chosen so that q(a)=ξ.

Facts & Assumptions

Given: A disc D(a,r) with r>0, a nowhere-zero holomorphic function h on it, a natural m≥1, and, for the normalized form, a scalar ξ satisfying ξm=h(a). The complex exponential is entire (The complex exponential is entire and its complex derivative is itself), holomorphic compositions obey the complex chain rule (The chain rule for complex derivatives), and every nonzero complex number has exactly m distinct mth roots (The n-th roots of a complex number and the n distinct roots of unity for every n≥1).

[L1]

If h is nowhere zero and holomorphic on a disc, then there is a holomorphic L on that disc with exp⁡L=h (A nonvanishing holomorphic function on a disc has a holomorphic logarithm).

[L2]

For all complex z,w, exp⁡(z+w)=exp⁡zexp⁡w (exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential).

Proof

technique · direct
1.1L1

Take from [L1] a holomorphic function L with exp⁡L=h.

2.1step 1.1L2givenalgebra

Because m≥1, division by m is defined. Put q:=exp⁡(L/m). Repeated use of [L2] gives qm=exp⁡L=h, and q is holomorphic; for m=1 this construction gives q=h.

3.1step 1.1step 2.1givenalgebra∎

For the prescribed value, both q(a) and ξ are nonzero and have mth power h(a). Thus c:=ξ/q(a) satisfies cm=1, and q~:=cq is holomorphic with q~m=h and q~(a)=ξ.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A nonzero complex derivative gives a local biholomorphism

Statement

If f is holomorphic near a and f′(a)≠0, then f is biholomorphic between neighbourhoods of a and f(a).

On suitable complex domains V and W with a∈V and f(a)∈W, the restriction f∣V:V→W is biholomorphic (Biholomorphic maps between complex domains), and its inverse g satisfies g′(w)=1f′(g(w))(w∈W).

Facts & Assumptions

Given: A holomorphic function f on an open neighbourhood of a with f′(a)≠0. Holomorphic functions are smooth as real maps near a (Holomorphic functions are real analytic and smooth in their two real coordinates).

[L1]

For a holomorphic map f=u+iv, its real Jacobian determinant is ∣f′∣2, and this determinant is positive exactly where f′≠0 (The Jacobian determinant of a holomorphic map is ∣f′∣2 and is positive exactly where f′≠0).

[L2]

If a C1 map between open subsets of Rn has invertible derivative at a, then it restricts to a C1 bijection between open neighbourhoods, whose inverse g satisfies Dg(y)=Df(g(y))−1 (The Euclidean inverse function theorem).

[L3]

A real totally differentiable plane map is complex differentiable exactly when its real derivative is multiplication by a complex number; that number is its complex derivative (Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with ∂zˉf=0, or with the Cauchy–Riemann equations).

[L4]

A continuous image of a connected space is connected (A continuous image of a connected space is connected, and connectedness is a topological property, claim 1).

[L5]

A segment t↦(1−t)v0+tv1 that lies in a subset A is a continuous path in A, and a path-connected subset of a topological space is a connected subset (A finite concatenation of straight segments in Rn is a continuous path, Every path-connected space is connected, and every path component lies inside a component, claim 2).

Proof

technique · direct
1.1L1given

By [L1], det⁡Df(a)=∣f′(a)∣2>0, so the real derivative Df(a) is invertible.

2.1step 1.1L2

Apply [L2] to the underlying smooth real map: there are open neighbourhoods V0 of a and W0 of f(a) such that f∣V0:V0→W0 is bijective with a C1 inverse g.

3.1step 2.1L3algebra

At every w∈W0, the derivative Df(g(w)) is multiplication by f′(g(w)) by [L3], and it is invertible by the inverse-function construction. Hence Dg(w)=Df(g(w))−1 is multiplication by 1/f′(g(w)); [L3] makes g complex differentiable there with the displayed derivative.

4.1step 2.1step 3.1L4L5given∎

Choose a disc V centred at a with closure contained in V0, and put W:=f[V]. The disc V is nonempty and open, and the triangle inequality keeps the segment between any two of its points inside it, so [L5] makes V connected and hence a complex domain. The homeomorphism f∣V0 makes W open, while [L4] makes it connected as the continuous image of V. Thus V and W are complex domains, and steps 2.1 and 3.1 show that f∣V and its inverse are holomorphic. Hence f∣V:V→W is biholomorphic.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Local normal form of a nonconstant holomorphic map

Statement

Let f:Ω→C be nonconstant and holomorphic on a complex domain Ω, let a∈Ω, and put m=deg⁡af. Then near a there is a biholomorphic coordinate ϕ with ϕ(a)=0 and f(z)−f(a)=ϕ(z)m.

Precisely, there is a complex domain V with a∈V⊆Ω such that ϕ:V→ϕ[V] is biholomorphic, ϕ(a)=0, and the displayed identity holds for every z∈V.

Facts & Assumptions

Given: A nonconstant holomorphic function f on a complex domain Ω, a point a∈Ω, and the positive natural m=deg⁡af (Local degree of a nonconstant holomorphic map). Holomorphic products obey the product rule (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L1]

A holomorphic function has finite order m at a exactly when, near a, it has the form (z−a)mh(z) with h holomorphic and h(a)≠0 (The order of a zero is the exponent in its local holomorphic factorization).

[L2]

For every positive natural m, a nowhere-zero holomorphic function on a disc has a holomorphic mth root (Holomorphic roots of a nonvanishing function on a disc).

[L3]

If a function is holomorphic near a and has nonzero derivative at a, then it is biholomorphic between neighbourhoods of a and its value (A nonzero complex derivative gives a local biholomorphism).

[L4]

A complex differentiable function is continuous at every point of complex differentiability (Complex differentiability at a point implies continuity there).

Proof

technique · direct
1.1L1given

Apply [L1] to f−f(a): on a neighbourhood of a one has f(z)−f(a)=(z−a)mh(z), where h is holomorphic and h(a)≠0.

2.1step 1.1L2L4

Since h(a)≠0, [L4] permits shrinking to a disc on which h is nowhere zero. By [L2] there is a holomorphic q on that disc with qm=h.

3.1step 2.1L3givenalgebra

Define ϕ(z):=(z−a)q(z). Then ϕ(a)=0 and the product rule gives ϕ′(a)=q(a)≠0, so [L3] makes ϕ biholomorphic after one further shrinking around a.

4.1step 1.1step 2.1step 3.1algebra∎

On that final neighbourhood, steps 1.1 and 2.1 give f(z)−f(a)=(z−a)mq(z)m=ϕ(z)m, which is the required normal form.

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A local degree-m holomorphic map has m nearby sheets

Statement

Let f:Ω→C be nonconstant and holomorphic on a complex domain Ω, let a∈Ω, and put m=deg⁡af. After shrinking around a, every nearby value other than f(a) has exactly m distinct preimages.

Precisely, for every neighbourhood N of a in Ω, there are an open neighbourhood V of a with V⊆N and a real ρ>0 such that, for every w with 0<∣w−f(a)∣<ρm, the equation f(z)=w has exactly m distinct solutions in V. The value f(a) has the single preimage a in V, counted with multiplicity m.

Facts & Assumptions

Given: A nonconstant holomorphic function f:Ω→C on a complex domain, a point a∈Ω, the positive natural m=deg⁡af (Local degree of a nonconstant holomorphic map), and an arbitrary neighbourhood N of a in Ω. A biholomorphism is bijective with holomorphic inverse (Biholomorphic maps between complex domains).

[L1]

If f:Ω→C is nonconstant and holomorphic on a complex domain, a∈Ω, and m=deg⁡af, then near a there is a biholomorphic coordinate ϕ with ϕ(a)=0 and f(z)−f(a)=ϕ(z)m (Local normal form of a nonconstant holomorphic map).

[L2]

Every nonzero complex number has exactly m distinct mth roots when m≥1, while 0 has the single mth root 0 (The n-th roots of a complex number and the n distinct roots of unity for every n≥1).

Proof

technique · direct
1.1L1givenchoose

Take a complex domain V0 and biholomorphic coordinate ϕ from [L1]. Since N is a neighbourhood of a, choose an open set O with a∈O⊆N. The set ϕ[V0∩O] is open and contains 0, so choose ρ>0 with D(0,ρ)⊆ϕ[V0∩O] and put V:=ϕ−1[D(0,ρ)]⊆N.

2.1step 1.1L2

If 0<∣w−f(a)∣<ρm, then [L2] gives exactly m distinct roots u of um=w−f(a), and each satisfies ∣u∣=∣w−f(a)∣1/m<ρ.

3.1step 1.1step 2.1L2given

Since ϕ is bijective, its inverse transports those roots to exactly m distinct points z∈V satisfying f(z)=w. At w=f(a), [L2] says the only coordinate root is 0, so the only point is a=ϕ−1(0), and the normal form records multiplicity m.

4.1step 2.1step 3.1∎

Thus every noncentral value in the stated target disc has exactly m distinct preimages in V, while the central value has the one preimage of multiplicity m.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Open mapping theorem for holomorphic functions

Statement

Every nonconstant holomorphic function on a complex domain is an open map.

Thus, if f:Ω→C is nonconstant and holomorphic on a complex domain Ω, then f[O] is open in C for every open subset O⊆Ω (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

Facts & Assumptions

Given: A nonconstant holomorphic function f on a complex domain Ω (A complex domain is a nonempty connected open subset of C) and an open subset O⊆Ω.

[L1]

If two holomorphic functions on a complex domain agree on a set with an accumulation point in the domain, then they agree everywhere on the domain (Identity theorem for holomorphic functions).

[L2]

If Ω is a complex domain, f:Ω→C is nonconstant and holomorphic, a∈Ω, and m=deg⁡af, then near a there is a biholomorphic coordinate ϕ with ϕ(a)=0 and f(z)−f(a)=ϕ(z)m (Local normal form of a nonconstant holomorphic map).

[L3]

If Ω is a complex domain, f:Ω→C is nonconstant and holomorphic, a∈Ω, and m=deg⁡af, then every neighbourhood N of a contains an open neighbourhood V for which some ρ>0 gives exactly m preimages in V for 0<∣w−f(a)∣<ρm, while f(a) has only the preimage a, counted with multiplicity m (A local degree-m holomorphic map has m nearby sheets).

Proof

technique · direct
1.1L1given

The function f is not constant on any neighbourhood of any a∈Ω: if it were constant on one, [L1] would make it constant on the connected domain Ω.

2.1step 1.1L2L3

Fix a∈O. Shrink the neighbourhood in [L2] so that it lies in O. The local multiplicity conclusion [L3], including its central value, gives a disc about f(a) contained in the image of that neighbourhood and therefore in f[O].

3.1step 2.1∎

Every point of f[O] is therefore interior. Hence f[O] is open; when O=∅, its image is empty and the same conclusion holds.

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Complex-analytic and Banach-space open mapping theorems

The complex-analytic open mapping theorem, Open mapping theorem for holomorphic functions, concerns a nonconstant holomorphic function on a complex domain. Its conclusion comes from the local power form of a one-variable holomorphic map.

The Banach-space result documented in the references has different hypotheses and a different proof: it concerns a surjective bounded linear map between complete normed spaces. It is not used here, and neither theorem is a specialization of the other despite the shared name.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Local maximum modulus principle

Statement

If the modulus of a holomorphic function on a complex domain has an interior local maximum, then the function is constant.

Precisely, if f is holomorphic on a complex domain Ω and there are a∈Ω and a neighbourhood V⊆Ω of a such that ∣f(z)∣≤∣f(a)∣ for every z∈V, then f is constant on Ω.

Facts & Assumptions

Given: A holomorphic function f on a complex domain Ω, a point a∈Ω, and a neighbourhood V on which ∣f(z)∣≤∣f(a)∣. The modulus obeys the usual multiplicative and positivity laws (Conjugation is an involutive real-field automorphism, zz‾=∣z∣2, and modulus is definite, multiplicative, and subadditive).

[L1]

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

Proof

technique · direct
1.1L1given

Suppose f is nonconstant. Choose an open disc D about a contained in V. By [L1], f[D] is an open set containing f(a), so it contains a disc D(f(a),ρ) for some ρ>0.

2.1step 1.1algebra

If f(a)≠0, the point w=(1+t)f(a) lies in D(f(a),ρ) and has ∣w∣>∣f(a)∣ for sufficiently small t>0. If f(a)=0, any nonzero w with ∣w∣<ρ has larger modulus. Thus in either case f[D] contains a value whose modulus is greater than ∣f(a)∣.

3.1step 1.1step 2.1∎

Step 2.1 contradicts the local maximum on V. Hence f cannot be nonconstant and must be constant on Ω.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Maximum principle for the real part of a holomorphic function

Statement

If the real part of a holomorphic function on a complex domain has an interior local maximum, then the function is constant.

That is, if f is holomorphic on a complex domain Ω and Re⁡f(z)≤Re⁡f(a) throughout some neighbourhood of a∈Ω, then f is constant on Ω.

Facts & Assumptions

Given: A holomorphic function f on a complex domain Ω, a point a∈Ω, and a neighbourhood V on which Re⁡f(z)≤Re⁡f(a).

[L1]

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

Proof

technique · direct
1.1L1given

Suppose f is nonconstant. For a disc D about a contained in V, [L1] makes f[D] an open neighbourhood of f(a), so D(f(a),ρ)⊆f[D] for some ρ>0.

2.1step 1.1algebra

The point f(a)+ρ/2 belongs to that target disc and has real part Re⁡f(a)+ρ/2>Re⁡f(a), so some point of D violates the assumed local maximum.

3.1step 1.1step 2.1∎

The contradiction in step 2.1 rules out nonconstancy, so f is constant on Ω.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Boundary maximum modulus principle on a bounded domain

Statement

If Ω is a bounded complex domain and f is continuous on Ω‾ and holomorphic on Ω, then ∣f∣ attains its maximum on ∂Ω.

Equivalently, there is ζ∈∂Ω such that ∣f(z)∣≤∣f(ζ)∣(z∈Ω‾).

Facts & Assumptions

Given: A bounded complex domain Ω and a continuous function f:Ω‾→C whose restriction to Ω is holomorphic. The complex-plane topology and Euclidean-plane topology agree (C=R[x]/(x2+1) as the Euclidean plane and as a normed real algebra: what the identification preserves).

[L1]

If the modulus of a holomorphic function on a complex domain has an interior local maximum, then the function is constant (Local maximum modulus principle).

[L3]

A continuous real-valued function on a nonempty compact metric space has a maximum and a minimum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

Proof

technique · direct
1.1L2L3givenalgebra

The closure Ω‾ is nonempty, closed, and bounded in the Euclidean plane, hence compact by [L2]. The reverse triangle inequality and continuity of f make ∣f∣ continuous there, so [L3] gives a maximizer z0∈Ω‾.

2.1step 1.1L1

If z0∈Ω, then ∣f∣ has an interior local maximum, and [L1] makes f constant on Ω.

3.1step 1.1step 2.1L4given

If z0∉Ω, then z0∈∂Ω. In the remaining branch f is constant on Ω by step 2.1 and hence on Ω‾ by continuity. The boundary is nonempty: otherwise the nonempty open set Ω would also be closed in the connected plane [L4] and therefore equal the unbounded plane. Thus any boundary point has the same modulus as z0.

4.1step 3.1∎

In either branch, a point of ∂Ω carries the global maximum of ∣f∣ on Ω‾.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Maximum modulus principle with boundary and infinity control

Statement

Boundary control together with control at infinity bounds the modulus throughout an unbounded complex domain.

In full, let Ω be a complex domain, let f:Ω→C be holomorphic, and let M≥0. Suppose that for every ε>0:

  • for every ζ∈∂Ω, some neighbourhood Vζ satisfies ∣f(z)∣<M+ε for all z∈Vζ∩Ω;
  • if Ω is unbounded, some R>0 satisfies ∣f(z)∣<M+ε whenever z∈Ω and ∣z∣>R.

Then ∣f(z)∣≤M for every z∈Ω. For bounded Ω, only the finite-boundary clause is required.

Facts & Assumptions

Given: A complex domain Ω, a holomorphic function f on it, a real M≥0, and the two stated control hypotheses. The complex and Euclidean plane topologies agree (C=R[x]/(x2+1) as the Euclidean plane and as a normed real algebra: what the identification preserves), and closure and boundary have the meanings of Interior, closure, boundary, limit point, isolated point and dense subset of a metric space.

[L1]

If the modulus of a holomorphic function on a complex domain has an interior local maximum, then the function is constant (Local maximum modulus principle).

[L3]

A continuous real-valued function on a nonempty compact metric space attains a maximum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[L5]

A complex differentiable function is continuous at every point of complex differentiability (Complex differentiability at a point implies continuity there).

Proof

technique · direct
1.1given

Fix ε>0 and form the superlevel set Kε:={z∈Ω:∣f(z)∣≥M+ε}.

2.1step 1.1L2L5givenalgebra

By [L5] and the reverse triangle inequality, ∣f∣ is continuous, so Kε is relatively closed in Ω: at a point where ∣f∣<M+ε, that strict inequality persists on a neighbourhood. Boundary control excludes every point of ∂Ω from the closure of Kε, so Kε is closed in the plane. It is bounded because Ω is bounded or, in the unbounded case, because infinity control excludes all points with sufficiently large modulus. Thus [L2] makes Kε compact and it lies entirely inside Ω.

3.1step 2.1L3L1L4

If Kε were nonempty, [L3] would give a maximizer of ∣f∣ on it. Outside Kε the modulus is smaller than M+ε, so this is also an interior global maximum on Ω; [L1] makes f constant. When Ω is bounded, its boundary is nonempty because otherwise it would be a nonempty clopen subset of the connected plane [L4] and hence the whole unbounded plane, so the constant contradicts finite-boundary control. When Ω is unbounded, it contradicts infinity control. Hence Kε is empty.

4.1step 3.1algebra∎

The set Kε is empty for every ε>0. If some z had ∣f(z)∣>M, taking ε=(∣f(z)∣−M)/2 would put z in Kε, a contradiction; therefore ∣f∣≤M on Ω.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Minimum modulus principle for a nowhere-zero holomorphic function

Statement

A nowhere-zero holomorphic function on a complex domain cannot have an interior local modulus minimum unless it is constant.

Equivalently, if f is holomorphic and nowhere zero on a complex domain Ω and ∣f(z)∣≥∣f(a)∣ on some neighbourhood of a∈Ω, then f is constant.

Facts & Assumptions

Given: A nowhere-zero holomorphic function f on a complex domain Ω and an interior local minimum of ∣f∣ at a. The modulus is multiplicative, so ∣1/f∣=1/∣f∣ (Conjugation is an involutive real-field automorphism, zz‾=∣z∣2, and modulus is definite, multiplicative, and subadditive).

[L1]

If the modulus of a holomorphic function on a complex domain has an interior local maximum, then the function is constant (Local maximum modulus principle).

[L2]

A nowhere-zero holomorphic function has a holomorphic reciprocal (Linearity, product, reciprocal, and quotient rules for complex derivatives).

Proof

technique · direct
1.1L2given

Since f is nowhere zero, [L2] makes 1/f holomorphic throughout Ω.

2.1step 1.1L1algebra

The local inequality ∣f(z)∣≥∣f(a)∣>0 is equivalent to ∣1/f(z)∣≤∣1/f(a)∣, so ∣1/f∣ has an interior local maximum at a. By [L1], 1/f is constant.

3.1step 2.1algebra∎

The reciprocal of that nonzero constant is f, so f is constant on Ω.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Constant boundary modulus forces an interior zero or constancy

Statement

If a holomorphic function has constant modulus on the boundary of a bounded domain, then it is constant or has a zero in the domain.

Precisely, let Ω be a bounded complex domain and let f be continuous on Ω‾ and holomorphic on Ω. If ∣f(ζ)∣=M for every ζ∈∂Ω, then either f is constant on Ω or some a∈Ω satisfies f(a)=0.

Facts & Assumptions

Given: A bounded complex domain Ω, a function f continuous on Ω‾ and holomorphic on Ω, and a real M≥0 such that ∣f∣=M on ∂Ω. A nonvanishing holomorphic function has a holomorphic reciprocal (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L1]

If Ω is a bounded complex domain and f is continuous on Ω‾ and holomorphic on Ω, then ∣f∣ attains its maximum on ∂Ω (Boundary maximum modulus principle on a bounded domain).

[L2]

A nowhere-zero holomorphic function on a complex domain cannot have an interior local modulus minimum unless it is constant (Minimum modulus principle for a nowhere-zero holomorphic function).

Proof

technique · direct
1.1L1given

If M=0, then [L1] gives ∣f∣≤0 on Ω‾, so f is the zero function and is constant.

1.2L1givenalgebra

Suppose M>0 and f has no zero in Ω. On ∂Ω one has ∣f∣=M>0, so f has no zero on Ω‾. At a point c∈Ω‾ the identity 1/f(z)−1/f(c)=(f(c)−f(z))/(f(z)f(c)) together with ∣f(z)∣≥∣f(c)∣/2 for z near c bounds ∣1/f(z)−1/f(c)∣ by 2∣f(z)−f(c)∣/∣f(c)∣2, so 1/f is continuous on Ω‾; the given reciprocal law makes it holomorphic on Ω. Applying [L1] to f and to 1/f gives ∣f∣≤M and 1/∣f∣≤1/M on Ω‾. Hence ∣f∣=M throughout Ω.

2.1step 1.2L2

The equality in step 1.2 makes every interior point a local minimum of ∣f∣, so [L2] makes f constant.

3.1step 1.1step 1.2step 2.1∎

Thus the zero-boundary case is constant, and in the positive-boundary case either f is constant or the supposition in step 1.2 fails and f has a zero in Ω.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Maximum principle on a closed strip for bounded holomorphic functions

Statement

A bounded function continuous on the closed strip, holomorphic inside, and of modulus at most one on both boundary lines has modulus at most one throughout the strip.

Precisely, let S={z∈C:0≤Re⁡z≤1}. If g:S→C is bounded and continuous, is holomorphic on 0<Re⁡z<1, and satisfies ∣g(iy)∣≤1,∣g(1+iy)∣≤1(y∈R), then ∣g(z)∣≤1 for every z∈S.

Facts & Assumptions

Given: The closed strip S and a function g satisfying the hypotheses. The exponential is entire, holomorphic compositions obey the chain rule, and the real exponential tends to 0 at −∞ (The complex exponential is entire and its complex derivative is itself, The chain rule for complex derivatives, The exponential tends to +∞ at +∞ and to 0 at −∞).

[L1]

If Ω is a bounded complex domain and f is continuous on Ω‾ and holomorphic on Ω, then ∣f∣ attains its maximum on ∂Ω (Boundary maximum modulus principle on a bounded domain).

[L3]

A segment t↦(1−t)v0+tv1 that lies in a subset A is a continuous path in A, and a path-connected subset of a topological space is a connected subset (A finite concatenation of straight segments in Rn is a continuous path, Every path-connected space is connected, and every path component lies inside a component, claim 2).

Proof

technique · direct
1.1L2givenalgebra

Fix ε>0 and define gε(z):=g(z)exp⁡(ε(z2−1)). By [L2], ∣gε(x+iy)∣=∣g(x+iy)∣exp⁡(ε(x2−y2−1)). On x=0 the exponential factor is at most 1, and on x=1 it is exp⁡(−εy2)≤1, so both vertical boundary lines retain modulus at most 1.

2.1step 1.1givenchoose

Choose C≥0 with ∣g∣≤C. Since x2−1≤0 for 0≤x≤1, the horizontal sides at heights y=±T satisfy ∣gε(x±iT)∣≤Cexp⁡(−εT2). For all sufficiently large T, this is at most 1.

3.1step 2.1L1L3

The rectangle RT:={z:0<Re⁡z<1, ∣Im⁡z∣<T} is bounded, open and nonempty, and each coordinate of a segment between two of its points stays between that coordinate's endpoints, so the segment stays in RT and [L3] makes RT connected; it is therefore a bounded complex domain. With T as in step 2.1, all four boundary sides of RT have ∣gε∣≤1. The boundary maximum theorem [L1] therefore gives ∣gε∣≤1 throughout RT‾.

4.1step 3.1givenalgebra∎

Given z∈S, choose such a T>∣Im⁡z∣. Step 3.1 yields ∣g(z)∣≤exp⁡(−εRe⁡(z2−1)). Letting ε decrease to 0 gives ∣g(z)∣≤1. This also covers both vertical boundary lines and the zero function.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Hadamard three-lines theorem

Statement

For a bounded function continuous on the closed strip and holomorphic inside, the vertical-line supremum is log-convex.

Precisely, let S={z:0≤Re⁡z≤1}, let f:S→C be bounded and continuous and holomorphic on the open strip, and define M(x):=sup⁡y∈R∣f(x+iy)∣(0≤x≤1). Then, for 0<θ<1, M(θ)≤M(0)1−θM(1)θ. More generally, for 0≤x0<x1≤1 and 0<t<1, M((1−t)x0+tx1)≤M(x0)1−tM(x1)t. Both displayed inequalities are asserted only for strictly interior parameters, 0<θ<1 and 0<t<1, so both exponents are strictly positive and the positive-exponent convention 0s=0 applies when a boundary supremum is zero (Real powers for positive bases, with the zero-base positive-exponent convention); the excluded endpoint expressions M(0)0 and M(1)0 would be the undefined 00 when that supremum vanishes.

Facts & Assumptions

Given: The strip S, a function f satisfying the hypotheses, and the finite nonnegative suprema M(x), whose existence follows from boundedness and completeness (Dedekind completeness: the least-upper-bound property). The complex exponential is entire (The complex exponential is entire and its complex derivative is itself), holomorphic compositions obey the complex chain rule (The chain rule for complex derivatives), and the exponential addition law, positive-base logarithm laws, and continuity of real powers are supplied by exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential, The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, and Continuity and derivatives of positive-base real powers.

[L1]

A bounded function continuous on the closed strip, holomorphic inside, and of modulus at most one on both boundary lines has modulus at most one throughout the strip (Maximum principle on a closed strip for bounded holomorphic functions).

[L2]

For a>0 and real x, the real power is ax=exp⁡(xlog⁡a) (Real powers for positive bases, with the zero-base positive-exponent convention).

[L3]

For nonzero complex z and complex w, the principal power is zprw=exp⁡(wLog⁡z) (Complex logarithms, the principal logarithm, and principal and multivalued complex powers).

Proof

technique · direct
1.1L2L3given

Fix δ>0 and define Gδ(z):=f(z)exp⁡((z−1)log⁡(M(0)+δ))exp⁡(−zlog⁡(M(1)+δ)). This is the positive-base principal-power normalization of [L2] and [L3]; it is bounded and continuous on S and holomorphic inside.

2.1step 1.1L1givenalgebra

On z=iy, the two exponential factors have moduli (M(0)+δ)−1 and 1, so ∣Gδ(iy)∣≤M(0)/(M(0)+δ)≤1. On z=1+iy, their moduli are 1 and (M(1)+δ)−1, so the same bound holds. By [L1], ∣Gδ(z)∣≤1 throughout S.

3.1step 2.1L2givenalgebra

At z=θ+iy with 0<θ<1, step 2.1 rearranges to ∣f(z)∣≤(M(0)+δ)1−θ(M(1)+δ)θ. Taking the supremum over y and letting δ decrease to 0 gives M(θ)≤M(0)1−θM(1)θ. Both exponents 1−θ and θ are strictly positive, so the limit is correct including either zero boundary supremum, where the convention of [L2] reads the vanishing factor as 0.

4.1step 3.1algebra∎

For 0≤x0<x1≤1, apply step 3.1 to the rescaled strip function w↦f(x0+(x1−x0)w). Its boundary suprema are M(x0) and M(x1), so the resulting inequality is the asserted log-convexity at (1−t)x0+tx1.

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Hadamard three-lines and complex interpolation

The normalization in Hadamard three-lines theorem is the scalar mechanism behind complex interpolation arguments. One builds a bounded holomorphic scalar function on a strip, estimates its two boundary lines, and lets the three-lines inequality interpolate the interior exponent. Turning that mechanism into an operator interpolation theorem requires additional normed-space and duality hypotheses; no such operator theorem is asserted here.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Holomorphic inverse function theorem and local-degree criterion

Statement

For a nonconstant holomorphic map, nonzero derivative, local degree one, local injectivity, and local biholomorphy are equivalent.

Precisely, let f be nonconstant and holomorphic on a complex domain Ω, and let a∈Ω. The following are equivalent:

  1. f′(a)≠0;
  2. deg⁡af=1 (Local degree of a nonconstant holomorphic map);
  3. f is locally injective at a (Locally injective holomorphic maps);
  4. f is biholomorphic between neighbourhoods of a and f(a) (Biholomorphic maps between complex domains).

For a local inverse g, one has g′(w)=1f′(g(w)) throughout its domain.

Facts & Assumptions

Given: A nonconstant holomorphic function f on a complex domain Ω and a point a∈Ω. The complex chain rule applies to inverse identities (The chain rule for complex derivatives).

[L1]

If f is holomorphic near a and f′(a)≠0, then f is biholomorphic between neighbourhoods of a and f(a) (A nonzero complex derivative gives a local biholomorphism).

[L2]

For every neighbourhood N of a, there are a smaller open neighbourhood V⊆N and a real ρ>0 such that every w with 0<∣w−f(a)∣<ρm, where m=deg⁡af, has exactly m distinct preimages in V (A local degree-m holomorphic map has m nearby sheets).

[L3]

A holomorphic function has finite order m at a exactly when, on some neighbourhood of a, it is (z−a)mq(z) with q holomorphic and q(a)≠0 (The order of a zero is the exponent in its local holomorphic factorization).

Proof

technique · direct
1.1L3givenalgebra

For the equivalence between claims 1 and 2, [L3] gives f(z)−f(a)=(z−a)mq(z) with m=deg⁡af and q(a)≠0. If m=1, differentiation at a gives f′(a)=q(a)≠0; if m>1, it gives f′(a)=0. Thus f′(a)≠0 exactly when deg⁡af=1.

1.2L1assume-hyp

For the implication from claim 1 to claim 4, [L1] directly makes f biholomorphic between neighbourhoods of a and f(a).

1.3assume-hyp

For the implication from claim 4 to claim 3, a biholomorphic restriction is bijective and hence injective on its source neighbourhood.

2.1L2step 1.1assume-hypchoose

For the converse implication from claim 3 back to claim 2, suppose f is injective on a neighbourhood N of a. If m=deg⁡af>1, take V⊆N and ρ>0 from [L2] and put w:=f(a)+ρm/2. Then w has m>1 distinct preimages in V, contradicting injectivity on N. Since m is positive, m=1, and step 1.1 then gives f′(a)≠0.

3.1step 1.2givenalgebra∎

For the derivative formula, let g be the inverse supplied in step 1.2. Differentiating g(f(z))=z gives g′(f(z))f′(z)=1, so, writing w=f(z), one obtains g′(w)=1/f′(g(w)).

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

An injective holomorphic map has no critical point and is biholomorphic onto its image

Statement

An injective holomorphic map on a complex domain has nowhere-zero derivative and is biholomorphic onto its open image.

Precisely, if f:Ω→C is holomorphic and injective on a complex domain, then f′(a)≠0 for every a∈Ω, the set f[Ω] is a complex domain, and f:Ω→f[Ω] is biholomorphic (Biholomorphic maps between complex domains).

Facts & Assumptions

Given: A holomorphic injective map f:Ω→C on a complex domain. Injectivity and bijectivity have their set-theoretic meanings (Injection, surjection, bijection).

[L1]

If f is nonconstant and holomorphic on a complex domain Ω and a∈Ω, then f′(a)≠0, deg⁡af=1, local injectivity at a, and biholomorphy between neighbourhoods of a and f(a) are equivalent (Holomorphic inverse function theorem and local-degree criterion).

[L2]

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

[L3]

A complex differentiable function is continuous at every point of complex differentiability (Complex differentiability at a point implies continuity there).

[L4]

A continuous image of a connected space is connected (A continuous image of a connected space is connected, and connectedness is a topological property, claim 1).

Proof

technique · direct
1.1L1given

The map f is nonconstant because an open complex domain has distinct points and f is injective. It is locally injective at every a∈Ω, so [L1] gives f′(a)≠0 and a holomorphic local inverse near f(a).

1.2L2L3L4given

By [L2], the image f[Ω] is open. By [L3], f is continuous, so [L4] makes its image connected; it is therefore a complex domain.

2.1step 1.1step 1.2

The global set-theoretic inverse f−1:f[Ω]→Ω agrees near every image point with the holomorphic local inverse from step 1.1. Hence f−1 is holomorphic throughout the image.

3.1step 2.1∎

The map f is bijective onto its image, and step 2.1 makes its inverse holomorphic; therefore it is biholomorphic onto the open image.

5 · Examples, counterexamples and false statements

None yet.

Sources