TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-08-29

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.

The principal logarithm is a biholomorphism from the slit plane to the principal strip

Statement

Let

$S : = C ∖ {x \in R : x \leq 0}, P : = {w \in C : - π < Im w < π} .$

Then the principal logarithm

$Log : S \to P$

is a biholomorphism.

Facts & Assumptions

Given: The slit plane $S$ and the principal strip $P$ above.

[F1]

On $S$ , the principal logarithm is holomorphic, satisfies $\exp (Log z) = z$ , and has imaginary part in $(- π, π)$ (The principal logarithm is the normalised holomorphic branch on the slit plane).

[F2]

The dictionary remark distinguishes the holomorphic principal branch on $S$ from the pointwise boundary value on the negative axis (Dictionary for holomorphic logarithm branches, the principal logarithm, and principal powers).

[F3]

The complex exponential is entire (The complex exponential is entire and its complex derivative is itself).

[F4]

For real $u, v$ , $\exp (u + i v) = e^{u} (\cos v + i \sin v)$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[F5]

A map is biholomorphic when it is bijective, holomorphic, and has holomorphic inverse (Biholomorphic maps between complex domains).

Proof

technique · direct

1.1F1F2given

By [F1] and [F2], $Log$ is holomorphic on $S$ and maps $S$ into $P$ .

2.1F1step 1.1algebra

If $Log z_{1} = Log z_{2}$ , then exponentiating and using [F1] gives $z_{1} = \exp (Log z_{1}) = \exp (Log z_{2}) = z_{2}$ . Thus $Log$ is injective.

3.1F1F4step 2.1algebra

If $w = u + i v \in P$ , then [F4] gives $\exp w = e^{u} (\cos v + i \sin v) \neq 0$ ; because $v \in (- π, π)$ , this value is never on the nonpositive real axis, so $\exp w \in S$ , and its principal logarithm is exactly $w$ . Hence $Log$ is surjective onto $P$ with inverse $w \mapsto \exp w$ .

4.1F3F5step 1.1step 3.1∎

The inverse $w \mapsto \exp w$ is holomorphic by [F3]. Therefore [F5] makes $Log : S \to P$ a biholomorphism.

Depends on

Used by

Dependency tree · two levels

38 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

Lars V. Ahlfors, Complex Analysis, 3rd ed., Ch. 3 §4.2 (standard reference, not scraped)
Jiri Lebl, Guide to Cultivating Complex Analysis, Exercise 4.1.1 (standard reference, not scraped)