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 function e^(1/z) omits zero and takes every nonzero value infinitely often near the origin
Example
The function
on omits and takes every nonzero value infinitely often near .
Facts & Assumptions
Given: The punctured-disc function .
The exponential maps onto (The complex exponential maps onto ).
Its fibres are the translates (, and exactly when ).
A removable singularity is bounded near the centre, a pole has modulus tending to infinity there, and every other isolated singularity is essential (Characterizations of removable singularities, Characterizations of poles, Every isolated singularity is removable, a pole, or essential).
Verification
Since the exponential never vanishes, never equals on the punctured disc.
Fix . By [L1] and [L2], choose with ; then every number is another logarithm of . Since as , for every sufficiently large it exceeds . For those infinitely many indices set ; then , , and . Thus every nonzero value occurs infinitely often within the punctured-disc domain near .
Along , , whereas along , . Both sequences eventually lie in the punctured disc, so is neither removable nor a pole, and hence is an essential singularity.
Therefore Great Picard is sharp: an essential singularity can omit one finite value, namely .
Depends on
- The complex exponential maps $\mathbb C$ onto $\mathbb C\setminus\{0\}$
- $\ker(\exp)=2\pi i\mathbb Z$, and $\exp z=\exp w$ exactly when $z-w\in2\pi i\mathbb Z$
- Great Picard theorem
- Every isolated singularity is removable, a pole, or essential
- Characterizations of removable singularities
- Characterizations of poles
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
24 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, §6.4 (standard reference, not scraped)