Alphabeta Math
Pipeline-generated
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.

✓ 12 results · all verified · 4 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 8 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Normal Families and Montel's Theorem

1 · Prerequisites

2 · Summary

This page metrizes local uniform convergence on a plane domain by a canonical compact exhaustion, proves that the resulting function-space topology is independent of the chosen exhaustion, and shows that continuous functions are complete and holomorphic functions closed for that topology. Those topological preliminaries are the bookkeeping that makes normality unambiguous rather than exhaustion-dependent.

The core complex-analysis content is the Montel package. Local boundedness gives local equicontinuity by Cauchy estimates, compact-domain Ascoli then yields Montel's theorem by diagonal extraction, and the same compactness pattern proves the Vitali-Porter theorem and continuity of derivative operators. The page closes by transporting the whole story to sphere-valued meromorphic maps through the chordal metric, including the compact-target Ascoli criterion needed later for meromorphic normal families.

3 · Logical flowchart

4 · Definitions, theorems and proofs

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Every plane domain has the canonical nested compact exhaustion by distance and radius cutoffs

Statement

Let Ω⊆C be a plane domain, and define for n≥1 Kn:={z∈Ω:∣z∣≤n and dist⁡(z,∂Ω)≥1/n}, with the convention dist⁡(z,∅)=∞ when Ω=C. Then each Kn is compact, one has Kn⊆int⁡Kn+1, and Ω=⋃n≥1Kn.

Facts & Assumptions

Given: A plane domain Ω and the sets Kn={z∈Ω:∣z∣≤n and dist⁡(z,∂Ω)≥1/n}.

Proof

technique · direct
1.1L1given

Each Kn is bounded by ∣z∣≤n and closed because limits preserve both the radius bound and the distance-to-boundary inequality, so [L1] makes each Kn compact; early members are allowed to be empty.

1.2givenalgebra

If z∈Kn, then ∣z∣<n+1 and dist⁡(z,∂Ω)>1/(n+1), so a small disc about z stays inside Kn+1. Hence Kn⊆int⁡Kn+1.

2.1givenchoose∎

If z∈Ω, openness gives a closed disc D‾(z,r)⊆Ω; choosing n>∣z∣ and 1/n<r puts z in Kn. Therefore ⋃n≥1Kn=Ω.

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Locally uniform convergence on a plane domain is the already-published compact-convergence notion

Remark

This page uses the already-published compact-convergence dictionary for local uniform convergence. Concretely, on a plane domain Ω, a sequence of continuous maps fn:Ω→C converges locally uniformly exactly when it converges uniformly on every compact subset of Ω (Locally uniform convergence on an open subset of the complex plane is compact convergence).

The point of the present page is not to redefine that notion, but to package it through a canonical compact exhaustion and the resulting weighted metric on function spaces.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

The exhaustion metric on a function space over a plane domain

Definition

Fix a plane domain Ω and a compact exhaustion (Kn)n≥1 of Ω; for this page the canonical exhaustion of Every plane domain has the canonical nested compact exhaustion by distance and radius cutoffs is the default choice. For functions f,g:Ω→C, set sn(f,g):={0,Kn=∅,sup⁡z∈Kn∣f(z)−g(z)∣,Kn≠∅. and define the exhaustion metric by dK(f,g):=∑n≥12−nmin⁡(1,sn(f,g)).

Here the supremum is taken in [0,∞], so sn(f,g)=+∞ is allowed, and min⁡(1,+∞):=1. Thus each summand is a real number in [0,2−n], so the series converges absolutely. The metric is used on spaces of continuous or holomorphic functions on Ω; the next theorem shows that its convergent sequences are exactly the locally uniformly convergent ones.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

The exhaustion metric induces exactly the topology of locally uniform convergence

Statement

Let (Kn) be the canonical compact exhaustion of a plane domain Ω, and let (fm) be a sequence of functions Ω→C. Then fm→f in dK⟺fm→f locally uniformly on Ω. Consequently the exhaustion metric induces exactly the topology of locally uniform convergence.

Facts & Assumptions

Given: The canonical exhaustion (Kn), the exhaustion metric dK, and a sequence fm:Ω→C.

[L1]

The sets Kn are compact, nested inside successive interiors, and exhaust Ω (Every plane domain has the canonical nested compact exhaustion by distance and radius cutoffs).

[L2]

On a plane domain, local uniform convergence is the same as uniform convergence on every compact subset (Locally uniform convergence on a plane domain is the already-published compact-convergence notion).

Proof

technique · direct
1.1givenalgebra

If dK(fm,f)→0, then each summand 2−nmin⁡(1,sn(fm,f)) tends to 0, so fm→f uniformly on every Kn.

2.1L1L2given

Any compact set L⊆Ω is contained in some KN because the interiors of the Kn cover Ω by [L1]. Step 1.1 then gives uniform convergence on every compact L, and [L2] makes the convergence locally uniform.

3.1L2givenalgebra∎

Conversely, if fm→f locally uniformly, then [L2] gives uniform convergence on every Kn, including the empty stages with zero supremum. A finite-head plus geometric-tail estimate then gives dK(fm,f)→0.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

The compact-open topology on C(Ω,C) is independent of the chosen compact exhaustion

Statement

Any two compact exhaustions of a plane domain Ω induce the same topology on C(Ω,C) by the weighted exhaustion metric. Equivalently, the compact-open topology on C(Ω,C) is independent of the chosen compact exhaustion.

Facts & Assumptions

Given: Two compact exhaustions of the same plane domain Ω.

[L1]

An exhaustion metric induces exactly local uniform convergence (The exhaustion metric induces exactly the topology of locally uniform convergence).

[L2]

On a metric domain and metric target, the compact-open topology is the topology of compact convergence (For a metric domain and a metric target the compact-open topology on C(X,Y) is the topology of compact convergence).

Proof

technique · direct
1.1L1given

By [L1], each exhaustion metric induces the same convergence notion, namely local uniform convergence on Ω.

2.1L2given∎

Fact [L2] identifies that convergence notion with compact convergence and hence with the compact-open topology on C(Ω,C). Therefore the induced topology is independent of the chosen exhaustion.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Continuous complex-valued functions on a plane domain are complete for an exhaustion metric

Statement

For a plane domain Ω, the space C(Ω,C) of continuous complex-valued functions is complete for the canonical exhaustion metric.

Facts & Assumptions

Given: A plane domain Ω, its canonical exhaustion (Kn), and a dK-Cauchy sequence (fm) in C(Ω,C).

[L1]

A sequence of complex-valued functions is uniformly Cauchy on a set if and only if it converges uniformly on that set (A sequence of complex-valued functions converges uniformly if and only if it is uniformly Cauchy).

[L2]

A uniform limit of continuous complex-valued functions is continuous (A uniform limit of continuous complex-valued functions is continuous).

[L3]

The canonical exhaustion is nested and its interiors exhaust Ω (Every plane domain has the canonical nested compact exhaustion by distance and radius cutoffs).

Proof

technique · direct
1.1L1L2given

On each Kn, the dK-Cauchy property makes (fm∣Kn) uniformly Cauchy; if Kn=∅ take the zero function there, and otherwise [L1] gives a uniform limit gn:Kn→C, which is continuous by [L2].

1.2L3given

The nesting of [L3] makes these limits compatible on overlaps, so they glue to a single function f:Ω→C. Because every point of Ω lies in the interior of some Kn by [L3], the glued function is continuous there.

2.1givenalgebra∎

Uniform convergence fm∣Kn→f∣Kn on each Kn, together with the usual finite-head and geometric-tail estimate in the defining series, gives dK(fm,f)→0. Thus C(Ω,C) is complete for the exhaustion metric.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Holomorphic functions form a closed subspace for locally uniform convergence

Statement

The holomorphic functions on a plane domain form a closed subspace of C(Ω,C) for the topology of locally uniform convergence. Equivalently, a dK-limit of holomorphic functions is holomorphic.

Facts & Assumptions

Given: A sequence of holomorphic functions converging in the exhaustion metric to a continuous limit f.

[L1]

Convergence in the exhaustion metric is exactly local uniform convergence (The exhaustion metric induces exactly the topology of locally uniform convergence).

Proof

technique · direct
1.1L1given

Fact [L1] turns the metric convergence into local uniform convergence on the domain.

2.1L2given∎

Applying [L2] shows that the limit function f is holomorphic. Hence holomorphic functions form a closed subspace for local uniform convergence.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Normal families of holomorphic functions on a plane domain

Definition

Let Ω⊆C be a plane domain and let F be a family of holomorphic functions on Ω. The family F is normal when every sequence (fn) in F has a subsequence (fnk) and a holomorphic function f on Ω such that fnk→f locally uniformly on Ω.

By Locally uniform convergence on a plane domain is the already-published compact-convergence notion, the same condition can be read as uniform convergence on every compact subset of Ω.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Locally bounded families of functions on a plane domain

Definition

Let Ω⊆C be a plane domain and let F be a family of functions Ω→C. The family F is locally bounded when for every a∈Ω there are a radius r>0 and a real M≥0 such that D‾(a,r)⊆Ωand∣f(z)∣≤M for every f∈F and every z∈D‾(a,r).

The bound M and neighbourhood may depend on a, but they are uniform over the whole family on that chosen neighbourhood.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Locally equicontinuous families of functions on a plane domain

Definition

Let Ω⊆C be a plane domain and let F be a family of functions Ω→C. The family F is locally equicontinuous when for every a∈Ω there is a radius r>0 with D‾(a,r)⊆Ω such that for every ε>0 there is δ>0 satisfying ∣z−w∣<δ⟹∣f(z)−f(w)∣<ε for every f∈F and every z,w∈D‾(a,r).

Thus the continuity modulus is shared by the whole family on some neighbourhood of each point.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Locally bounded holomorphic families are locally equicontinuous

Statement

Every locally bounded family of holomorphic functions on a plane domain is locally equicontinuous.

Facts & Assumptions

Given: A locally bounded family F of holomorphic functions on a plane domain Ω.

[L1]

Cauchy estimates bound derivatives on a smaller concentric disc from a common bound on a larger one (Cauchy estimates on a smaller concentric disc).

Proof

technique · direct
1.1L1given

Fix a∈Ω. Local boundedness gives a closed disc D‾(a,R)⊆Ω and a common bound ∣f∣≤M there for every f∈F. Applying [L1] to the inner disc D‾(a,R/2) gives the uniform derivative bound ∣f′(z)∣≤4M/R on that smaller disc.

2.1givenalgebra∎

The smaller closed disc is convex, so integrating f′ along the line segment from w to z yields ∣f(z)−f(w)∣≤(4M/R)∣z−w∣ for every f∈F. This is the local equicontinuity estimate.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Montel's theorem: every locally bounded holomorphic family is normal

Statement

Assume the Axiom of Choice, and therefore in particular Countable Choice and Dependent Choice for the successive subsequence selections. Let Ω be a plane domain and let F⊆H(Ω) be locally bounded. Then F is a normal family.

Facts & Assumptions

Given: Choice, a plane domain Ω, and a locally bounded family F⊆H(Ω).

[L1]

On a compact metric domain, compactness of the uniform closure is equivalent to equicontinuity and pointwise relative compactness (Ascoli–Arzelà in the uniform topology for nonempty compact metric domains).

[L2]

Holomorphic functions are closed under locally uniform limits (Holomorphic functions form a closed subspace for locally uniform convergence).

[L3]

The canonical exhaustion (Kn) is compact, nested, and has interiors covering Ω (Every plane domain has the canonical nested compact exhaustion by distance and radius cutoffs).

[L4]

Locally bounded holomorphic families are locally equicontinuous (Locally bounded holomorphic families are locally equicontinuous).

Proof

technique · direct
1.1L1L3L4given

On each compact stage Kn of [L3], local boundedness plus [L4] makes the restricted family equicontinuous and pointwise relatively compact; hence [L1] makes its uniform closure compact.

1.2L5givenchoose

Using [L5], choose successively a subsequence converging uniformly on K1, then a further subsequence converging uniformly on K2, and so on, and take the diagonal subsequence. This is the explicit Choice step named in the Statement.

1.3L3given

For each fixed m, the diagonal subsequence eventually lies in the mth chosen subsequence, so it converges uniformly on Km. Because the interiors of the Km cover Ω by [L3], this gives local uniform convergence on all of Ω.

2.1L2given∎

Fact [L2] makes the local uniform limit holomorphic, so every sequence in F has a locally uniformly convergent subsequence in H(Ω). That is exactly normality.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Normal holomorphic families are locally bounded

Statement

Assume the Axiom of Countable Choice. Every normal family of holomorphic functions on a plane domain is locally bounded.

Facts & Assumptions

Given: Countable Choice and a normal family F⊆H(Ω).

[L1]

Normality means that every sequence in F has a subsequence converging locally uniformly to a holomorphic limit (Normal families of holomorphic functions on a plane domain).

Proof

technique · direct
1.1givenchoose

If F were not locally bounded at some point, then on some closed disc there would be a sequence (fn) in F with sup⁡∣fn∣>n.

2.1L1givenalgebra∎

By [L1], a subsequence would converge uniformly on that disc to a holomorphic limit, and uniform convergence on a compact disc forces that subsequence to be uniformly bounded there. This contradicts step 1.1, so the family is locally bounded.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Vitali-Porter convergence theorem for holomorphic functions

Statement

Assume the Axiom of Choice. Let Ω be a plane domain and let (fn) be a locally bounded sequence in H(Ω). Suppose there is a set E⊆Ω with an accumulation point in Ω such that fn(z) converges for every z∈E. Then (fn) converges locally uniformly on Ω to a holomorphic function.

Facts & Assumptions

Given: Choice, a plane domain Ω, a locally bounded holomorphic sequence (fn), and a set E⊆Ω on which the pointwise limit exists with an accumulation point in Ω.

[L1]

Locally bounded holomorphic families are normal (Montel's theorem: every locally bounded holomorphic family is normal).

[L2]

Two holomorphic functions that agree on a set with an accumulation point in the domain agree everywhere (Identity theorem for holomorphic functions).

Proof

technique · direct
1.1L1L2given

By [L1], every subsequence of (fn) has a further subsequence converging locally uniformly to a holomorphic limit. Any two such subsequential limits agree on E, because the scalar sequence fn(z) has a fixed pointwise limit there, so [L2] makes them equal on all of Ω.

2.1L1givenassume-contradischarge-contradiction

If the whole sequence did not converge locally uniformly to that common limit, then some subsequence would stay a definite distance away on a compact set. Applying [L1] again to that subsequence would produce a further subsequence converging locally uniformly to the same limit from step 1.1, which is impossible.

3.1given∎

Therefore the full sequence converges locally uniformly on Ω to a holomorphic function.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Every derivative operator is continuous for locally uniform convergence on holomorphic functions

Statement

For every natural number k, including k=0, the operator Dk:H(Ω)→H(Ω),Dk(f)=f(k), is continuous for local uniform convergence on a plane domain Ω.

Facts & Assumptions

Given: A sequence fn→f locally uniformly in H(Ω).

[L1]

A locally uniform limit of holomorphic functions is holomorphic, and every derivative order converges locally uniformly as well (Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly).

Proof

technique · direct
1.1L1given

Fact [L1] gives fn(k)→f(k) locally uniformly on Ω for every natural k.

2.1given∎

This is exactly continuity of the operator Dk, and the case k=0 is included because D0 is the identity.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Chordal local uniform convergence and meromorphic normality

Definition

Let Ω⊆C be a plane domain and let fn,f:Ω→C^. The sequence (fn) converges chordally locally uniformly to f when for every compact set K⊆Ω, sup⁡z∈Kχ(fn(z),f(z))⟶0, where χ is the chordal metric of The chordal metric on the Riemann sphere. For the empty compact set the displayed supremum is defined to be 0.

A family F of meromorphic maps Ω→C^ is meromorphically normal when every sequence in F has a subsequence converging chordally locally uniformly either to a meromorphic map Ω→C^ or to the constant map ∞.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

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 fn→f 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.1L1givenchoosealgebra

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.

1.2L1givenchoosealgebra

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 gn→g into Euclidean local uniform convergence. Fact [L1] makes g holomorphic, so f is meromorphic at a.

2.1L2step 1.2given

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 g≡0 on V, so f≡∞ on V. Thus the ∞-value set of f is open in the holomorphic-input case.

3.1step 1.1step 1.2step 2.1given∎

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≡∞.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Local chordal equicontinuity is equivalent to meromorphic normality on compact exhaustions

Statement

Assume the Axiom of Choice, and therefore in particular Countable Choice and Dependent Choice for the successive subsequence selections. Let Ω be a plane domain and let F be a family of meromorphic maps Ω→C^. Then F is meromorphically normal⟺F∣K is equicontinuous for every compact K⊆Ω, where equicontinuity is taken with respect to the chordal metric on C^. Equivalently, it is enough to check that equicontinuity on each compact stage of the canonical exhaustion.

Facts & Assumptions

Given: Choice, a plane domain Ω, and a family F of meromorphic sphere-valued maps.

[L1]

On a compact metric domain, compactness of the uniform closure is equivalent to equicontinuity and pointwise relative compactness (Ascoli–Arzelà in the uniform topology for nonempty compact metric domains).

[L2]

The canonical exhaustion (Kn) is compact, nested, and has interiors covering Ω (Every plane domain has the canonical nested compact exhaustion by distance and radius cutoffs).

[L4]

A chordally locally uniform meromorphic limit is meromorphic or identically ∞ (A chordally locally uniform meromorphic limit is meromorphic or identically infinity).

Proof

technique · direct
1.1L1L2given

If the compact-set equicontinuity condition holds, then on each compact stage Kn of [L2] the restricted family is equicontinuous. Pointwise relative compactness is automatic because the target sphere is compact, so [L1] makes the uniform closure on Kn compact.

1.2L2L3L4givenchoose

Using [L3], choose successively a subsequence converging uniformly on K1, then on K2, and so on, and take the diagonal subsequence. By [L2] that diagonal converges chordally locally uniformly on Ω, and [L4] makes its limit meromorphic or identically ∞. Thus compact-set chordal equicontinuity implies meromorphic normality.

1.3L1L2L3given

Conversely, if F is meromorphically normal, then every sequence of restrictions to a fixed Kn has a uniformly convergent subsequence. Fact [L3] turns that sequential compactness into compactness of the restriction closure, and [L1] then gives equicontinuity on Kn. Because every compact subset of Ω lies in some stage of the exhaustion by [L2], the family is chordally equicontinuous on every compact subset.

2.1given∎

The first two steps prove the forward implication and step 1.3 proves the reverse implication, so the two conditions are equivalent.

5 · Examples, counterexamples and false statements

None yet.

Sources