LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30

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.

Two omitted finite values rule out an essential singularity

Statement

Assume the Axiom of Choice. Let $f$ be holomorphic on a punctured disc $0 < ∣ z - a ∣ < R$ and omit two distinct finite values there. Then $a$ is removable for $f$ or a pole; in particular, $a$ is not an essential singularity.

Facts & Assumptions

Given: The Axiom of Choice and a holomorphic map $f$ on $0 < ∣ z - a ∣ < R$ omitting two distinct finite values.

[A1]

The Axiom of Choice is available for the subsequence selection below (The Axiom of Choice).

[L1]

Assuming the Axiom of Choice, holomorphic families omitting $0$ and $1$ are chordally normal (Families omitting two values are chordally normal).

[L2]

A chordal limit of holomorphic functions is holomorphic or identically $\infty$ (A chordally locally uniform meromorphic limit is meromorphic or identically infinity).

[L3]

Boundary maximum modulus propagates a boundary bound to a bounded annulus (Boundary maximum modulus principle on a bounded domain).

[L4]

A bounded punctured-disc holomorphic function has a removable singularity (Characterizations of removable singularities).

[L5]

Every isolated singularity is removable, a pole, or essential (Every isolated singularity is removable, a pole, or essential).

[L6]

A punctured-disc holomorphic function has a pole exactly when its reciprocal extends holomorphically across the centre and vanishes there (Characterizations of poles).

Proof

technique · direct

1.1A1L1givenchoose

After an affine change of target, we may assume the omitted values are $0$ and $1$ . Choose radii $ρ_{n} ↓ 0$ with $2 ρ_{1} < R$ , and define $f_{n} (ζ) : = f (a + ρ_{n} ζ)$ on the fixed annulus $A : = {1 / 2 < ∣ ζ ∣ < 2}$ . Each $f_{n}$ omits $0$ and $1$ , so [A1] and [L1] give a chordally locally uniformly convergent subsequence on $A$ ; relabel it again as $(f_{n})$ , with the corresponding radii still written $(ρ_{n})$ .

2.1L2step 1.1cases

By [L2], the limit of that subsequence is either holomorphic on $A$ or identically $\infty$ . In the first case, chordal local uniform convergence to a finite holomorphic limit is Euclidean local uniform convergence on the unit circle, so there are $M > 0$ and $N$ with $∣ f (a + ρ_{n} ζ) ∣ \leq M$ for every $n \geq N$ and $∣ ζ ∣ = 1$ . In the second case, the same argument applied to the infinity chart gives $M > 0$ and $N$ with $∣ 1 / f (a + ρ_{n} ζ) ∣ \leq M$ for every $n \geq N$ and $∣ ζ ∣ = 1$ .

3.1L3L4step 2.1cases

In the first case, fix $n \geq N$ and apply [L3] to the bounded annulus $Ω_{n} : = {z : ρ_{n + 1} \leq ∣ z - a ∣ \leq ρ_{n}}$ . Step 2.1 bounds $∣ f ∣$ by $M$ on both boundary circles of $Ω_{n}$ , so $∣ f (z) ∣ \leq M$ throughout $Ω_{n}$ . As this holds for every $n \geq N$ , the function $f$ is bounded on $0 < ∣ z - a ∣ \leq ρ_{N}$ . Fact [L4] then makes $a$ removable.

3.2L3L4L6step 2.1cases

In the second case, apply the same annulus argument to $1 / f$ . Step 2.1 bounds $∣ 1 / f ∣$ by $M$ on both boundary circles of each $Ω_{n}$ for $n \geq N$ , hence throughout every such annulus. Therefore [L4] extends $1 / f$ holomorphically across $a$ . If the extension is nonzero at $a$ , then its reciprocal extends $f$ , so $a$ is removable for $f$ . If the extension vanishes at $a$ , [L6] makes $a$ a pole of $f$ .

4.1L5step 3.1step 3.2∎

Steps 3.1 and 3.2 show that only the removable and pole branches of [L5] can occur, so $a$ is not an essential singularity.

Depends on

Used by

Great Picard theorem Theorem

Dependency tree · two levels

31 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

Aleksander Simonic, The Ahlfors lemma and Picard's theorems, Theorem 14 (standard reference, not scraped)