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.

Casorati-Weierstrass theorem

Statement

Let $f$ have an essential singularity at $a$ . Then for every $r > 0$ with $0 < ∣ z - a ∣ < r$ in the domain of $f$ , the image $f ({0 < ∣ z - a ∣ < r})$ is dense in $C$ .

Equivalently, for every $w \in C$ and every $ε > 0$ , some point $z$ with $0 < ∣ z - a ∣ < r$ satisfies $∣ f (z) - w ∣ < ε$ .

Facts & Assumptions

Given: An essential singularity of $f$ at $a$ and a radius $r > 0$ with $f$ holomorphic on $0 < ∣ z - a ∣ < r$ .

[L1]

Essential means neither removable nor a pole (Every isolated singularity is removable, a pole, or essential).

[L2]

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

[L3]

A function on a punctured disc has a pole exactly when its modulus tends to infinity there (Characterizations of poles).

[L4]

Reciprocal and sum rules preserve holomorphy wherever the denominators stay nonzero (Linearity, product, reciprocal, and quotient rules for complex derivatives).

Proof

technique · contradiction

1.1

Suppose, for contradiction, that $f ({0 < ∣ z - a ∣ < r})$ is not dense in $C$ . Then some $w \in C$ and some $ε > 0$ satisfy $∣ f (z) - w ∣ \geq ε$ for every $z$ with $0 < ∣ z - a ∣ < r$ .

assume-contra

2.1

The function $g (z) : = 1 / (f (z) - w)$ is therefore holomorphic on $0 < ∣ z - a ∣ < r$ by [L4] and bounded there by $1 / ε$ .

step 1.1L4algebra

3.1

By [L2], the bounded function $g$ extends holomorphically across $a$ . If the extension satisfies $g (a) \neq 0$ , then $1 / g$ is holomorphic near $a$ and $f = w + 1 / g$ is removable there by [L4]. If instead $g (a) = 0$ , then $1 / g$ has a pole at $a$ by [L3], so $f = w + 1 / g$ has a pole there as well.

step 2.1L2L3L4

4.1

Either outcome in step 3.1 contradicts [L1], because an essential singularity is neither removable nor a pole. Therefore the assumption of step 1.1 is false, and every punctured neighbourhood image is dense in $C$ .

step 1.1step 3.1L1discharge-contradiction∎

Depends on

Used by

e^1/z has an essential singularity at 0 and omits the value 0 Counterexample

Dependency tree · two levels

14 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

David Greenfield, Rutgers Math 403 diary (standard reference, not scraped)
Jean-Baptiste Campesato, MAT334 course page and notes index (standard reference, not scraped)