Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)
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 sequence of real-valued functions converges uniformly if and only if it is uniformly Cauchy

Statement

Let XX be a set and let fk:X→Rf_k:X\to\mathbb{R} for every k∈Nk\in\mathbb{N}. Then (fk)(f_k) converges uniformly on XX to some f:X→Rf:X\to\mathbb{R} if and only if (fk)(f_k) is uniformly Cauchy on XX (Pointwise convergence, uniform convergence, and the uniformly Cauchy condition for sequences of real-valued functions).

Facts & Assumptions

Given: A set XX and a sequence of functions fk:X→Rf_k:X\to\mathbb{R}.

[A1]

Uniform convergence to ff means that for every real ε>0\varepsilon>0 there is NN such that ∣fk(x)−f(x)∣<ε|f_k(x)-f(x)|<\varepsilon for every k≥Nk\ge N and every x∈Xx\in X (Pointwise convergence, uniform convergence, and the uniformly Cauchy condition for sequences of real-valued functions).

[A2]

Uniform Cauchyness means that for every real ε>0\varepsilon>0 there is NN such that ∣fm(x)−fn(x)∣<ε|f_m(x)-f_n(x)|<\varepsilon for every m,n≥Nm,n\ge N and every x∈Xx\in X (Pointwise convergence, uniform convergence, and the uniformly Cauchy condition for sequences of real-valued functions).

[A3]

Pointwise convergence as defined through real sequences can equivalently be tested with every positive real error (Pointwise convergence, uniform convergence, and the uniformly Cauchy condition for sequences of real-valued functions).

[L1]

For reals u,vu,v, ∣u+v∣≤∣u∣+∣v∣|u+v|\le |u|+|v| (The triangle inequality).

[L2]

Every Cauchy sequence of reals converges to a real (The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges).

Proof

technique · direct
1.1

Suppose first that fk→ff_k\to f uniformly on XX, and let ε>0\varepsilon>0 be real. By [A1] choose NN with ∣fj(x)−f(x)∣<ε/2|f_j(x)-f(x)|<\varepsilon/2 for every j≥Nj\ge N and x∈Xx\in X. Thus, for m,n≥Nm,n\ge N and x∈Xx\in X, ∣fm(x)−fn(x)∣≤∣fm(x)−f(x)∣+∣f(x)−fn(x)∣<ε|f_m(x)-f_n(x)|\le |f_m(x)-f(x)|+|f(x)-f_n(x)|<\varepsilon. Since ε\varepsilon was arbitrary, (fk)(f_k) is uniformly Cauchy.

A1A2L1choosealgebra
1.2

Conversely, suppose that (fk)(f_k) is uniformly Cauchy on XX. For each x∈Xx\in X, [A2] makes (fk(x))(f_k(x)) a Cauchy real sequence; by [L2] it has a real limit f(x)f(x). These values define a function f:X→Rf:X\to\mathbb{R}.

A2L2construct
1.3

Under this converse assumption, let ε>0\varepsilon>0 be real and choose NN such that ∣fm(x)−fn(x)∣<ε/2|f_m(x)-f_n(x)|<\varepsilon/2 for every m,n≥Nm,n\ge N and every x∈Xx\in X.

A2choose
2.1

Fix k≥Nk\ge N and x∈Xx\in X. Pointwise convergence at xx gives a threshold MM such that ∣fn(x)−f(x)∣<ε/2|f_n(x)-f(x)|<\varepsilon/2 for n≥Mn\ge M. Choose n≥N,Mn\ge N,M. Then ∣fk(x)−f(x)∣≤∣fk(x)−fn(x)∣+∣fn(x)−f(x)∣<ε|f_k(x)-f(x)|\le |f_k(x)-f_n(x)|+|f_n(x)-f(x)|<\varepsilon.

step 1.2step 1.3A3L1choose
3.1

The index NN in step 1.3 is independent of kk and xx, so step 2.1 proves fk→ff_k\to f uniformly. Together with step 1.1 this proves both directions.

step 1.1step 2.1A1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 35 results over 8 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources