Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck pass
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.

Every meromorphic function on a plane domain is a quotient of holomorphic functions

Statement

Every meromorphic function on a plane domain is a quotient of holomorphic functions.

Facts & Assumptions

Given: A meromorphic function f on a plane domain Ω.

[L1]

A meromorphic function is holomorphic away from a discrete pole set (Meromorphic functions on a plane domain).

[L2]

Every effective divisor with locally finite positive support on a plane domain is the zero divisor of a nonzero holomorphic function (Every locally finite effective divisor on a plane domain is a holomorphic zero divisor).

[L3]

A locally bounded punctured singularity is removable (Characterizations of removable singularities).

Proof

technique · direct
1.1L1L2givenconstruct

Let P be the pole set of f, with multiplicities equal to its positive finite pole orders. Each x∈Ω∖P has a holomorphy neighbourhood disjoint from P, and each a∈P has an isolated-pole neighbourhood meeting P only at a. Hence every point of Ω has a neighbourhood meeting P in finitely many points. For a compact K⊆Ω, the family of all such open neighbourhoods covers K; a finite subcover shows that K∩P is finite. Thus [L2] applies. Choose a holomorphic function h on Ω whose zero divisor is exactly P.

2.1L1L3step 1.1algebra

On Ω∖P, define g:=fh. Near a pole a∈P, the zero of h has exactly the same order as the pole of f, so g is locally bounded on a punctured neighbourhood of a. By [L3], g extends holomorphically across every point of P.

3.1step 1.1step 2.1algebra∎

Away from P, one has f=g/h. Since both sides are meromorphic and agree on the dense open set Ω∖P, this quotient represents f on all of Ω.

Depends on

Used by

Dependency tree · two levels

25 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