Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-08-28
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.

A chordally locally uniform meromorphic limit is meromorphic or identically infinity

Statement

Let Ω be a plane domain, and let fn:ΩC^ be meromorphic functions converging chordally locally uniformly to a map f:ΩC^. Then f is meromorphic or identically . If every fn is holomorphic, then f is holomorphic or identically .

Facts & Assumptions

Given: A plane domain Ω and a chordally locally uniformly convergent sequence fnf of meromorphic maps to C^.

[L2]

A locally uniform limit of nowhere-zero holomorphic functions is either identically zero or nowhere zero (Hurwitz's zero-free limit theorem).

Proof

technique · direct
1.1

A local uniform limit of continuous maps into the metric space (C^,χ) is continuous, so f is chordally continuous. If f(a)C, choose a chordal neighbourhood U of f(a) whose closure misses . On U the chordal and Euclidean metrics are comparable, and continuity of f together with chordal local uniform convergence gives a neighbourhood V of a with f(V)fn(V)U for all large n. On V the maps fn have no poles, hence are holomorphic there, and [L1] makes the Euclidean local uniform limit f holomorphic near a.

L1givenchoosealgebra
1.2

If f(a)=, choose a chordal neighbourhood U of whose complement is a closed Euclidean disc. Continuity of f and chordal local uniform convergence give a neighbourhood V of a with f(V)fn(V)U for all large n. The infinity-chart expressions g=1/f and gn=1/fn are then well-defined holomorphic maps on V, and the same metric comparison turns gng into Euclidean local uniform convergence. Fact [L1] makes g holomorphic, so f is meromorphic at a.

L1givenchoosealgebra
2.1

When every fn is holomorphic, the functions gn of step 1.2 are holomorphic and nowhere zero on V. By [L2], their limit g is either identically 0 on V or nowhere zero. Because g(a)=0, one gets g0 on V, so f on V. Thus the -value set of f is open in the holomorphic-input case.

L2step 1.2given
3.1

If f takes some finite value, then steps 1.1 and 1.2 show that it is meromorphic at every point of Ω; otherwise f. In the holomorphic-input case, the finite-value set is open by step 1.1 and the -value set is open by step 2.1, so connectedness leaves only the two possibilities: f is holomorphic on all of Ω, or f.

step 1.1step 1.2step 2.1given

Depends on

Used by

Dependency tree · two levels

18 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