TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

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.

Dini's theorem: on a compact metric space a nondecreasing sequence of continuous real functions converging pointwise to a continuous limit converges uniformly

Statement

Let $(X, d)$ be a compact metric space (Open cover, subcover, compact metric space, and compact subset of a metric space), let $f_{k} : X \to R$ be continuous for every $k \in N$ (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form, $R$ carrying its usual metric, The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded), and suppose

$f_{k} (x) \leq f_{k + 1} (x) for every k \in N and every x \in X,$

so that the sequence is nondecreasing at every point (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences). Suppose further that $f_{k} (x) \to f (x)$ for every $x \in X$ (Limits and Cauchy sequences of reals) with the limit function $f : X \to R$ continuous. Then $(f_{k})$ converges to $f$ uniformly (Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on $Y^{X}$ and on $C (X, Y)$ ).

All four hypotheses are used. Compactness of $X$ , monotonicity of the sequence, continuity of every $f_{k}$ and continuity of the limit $f$ each enter the proof, and dropping any one of them makes the conclusion false; the companion page exhibits the failure when the limit is not continuous.

The nonincreasing form holds too, by applying the theorem to $(- f_{k})$ and $- f$ , which are continuous and nondecreasing at every point; the proof below is written for the nondecreasing direction only, and the Statement claims that direction.

No choice principle is used: the finite subcover produced below is returned as a list of indices by the indexed form of compactness (A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it).

Facts & Assumptions

Given: A compact metric space $(X, d)$ , continuous functions $f_{k} : X \to R$ with $f_{k} (x) \leq f_{k + 1} (x)$ for all $k$ and $x$ , a continuous $f : X \to R$ with $f_{k} (x) \to f (x)$ for every $x \in X$ , and $ι$ the canonical natural of $R$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[A1]

$f_{k} (x) \leq f_{k + 1} (x)$ for every $k \in N$ and every $x \in X$ .

[A2]

$f_{k} (x) \to f (x)$ in $R$ for every $x \in X$ , and $f$ and every $f_{k}$ are continuous.

[L1]

A sequence of reals with $x_{k} \leq x_{k + 1}$ for every $k$ is nondecreasing, that is $x_{j} \leq x_{m}$ whenever $j \leq m$ (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L2]

A convergent sequence of reals is bounded, and a nondecreasing sequence bounded above converges to the supremum of its range; limits of real sequences are unique (Every convergent sequence is bounded, A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum, A sequence has at most one limit, Lower bound, bounded below, bounded set, Complete ordered field (least-upper-bound property), Suprema and infima are unique).

[L3]

A supremum is an upper bound of its set (Complete ordered field (least-upper-bound property), Suprema and infima are unique).

[L4]

Continuity of $h : X \to R$ at $a$ : for every real $η > 0$ there is a real $δ > 0$ with $∣ h (x) - h (a) ∣ < η$ whenever $d (x, a) < δ$ (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form, Metric continuity characterisations, with countable choice for the sequential converse, The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, Absolute value in an ordered field).

[L5]

A subset of a metric space is open exactly when each of its points has a ball around it inside the subset (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not).

[L6]

$X$ is a compact subset of itself, so every family $(U_{i})_{i \in I}$ of open subsets of $X$ with $X = ⋃_{i} U_{i}$ has $n \in N$ and indices $i_{0}, \dots, i_{n} \in I$ with $X = U_{i_{0}} \cup \dots \cup U_{i_{n}}$ , unless $X = \emptyset$ (A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, claim 3, Open cover, subcover, compact metric space, and compact subset of a metric space).

[L7]

For $n \geq 1$ and natural numbers $k_{0}, \dots, k_{n - 1}$ there is $j^{*} < n$ with $k_{j} \leq k_{j^{*}}$ for every $j < n$ : the nonempty finite set of reals ${ι (k_{0}), \dots, ι (k_{n - 1})}$ has a maximum, attained at some index, and $ι$ is strictly increasing on $N$ , hence reflects the order (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set, Canonical naturals are positive and strictly increasing, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L8]

Uniform convergence of $(f_{k})$ to $f$ is: for every real $ε > 0$ there is $N \in N$ with $∣ f_{k} (x) - f (x) ∣ < ε$ for every $x \in X$ and every $k \geq N$ (Uniform convergence, and the topology of uniform convergence: the metric topology of the uniform metric on $Y^{X}$ and on $C (X, Y)$ , Convergence in the uniform metric is exactly uniform convergence: one $N$ serving every point, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

Proof

technique · direct

1.1

Fix $x \in X$ ; the sequence $(f_{k} (x))$ is nondecreasing by [A1] and [L1], and it converges by [A2], hence is bounded and in particular bounded above.

A1A2L1L2

1.2

Let $ε > 0$ be real and put $U_{k} : = {x \in X : f (x) - f_{k} (x) < ε}$ for $k \in N$ .

construct

2.1

By [L2] the sequence $(f_{k} (x))$ converges to the supremum of its range, and by [A2] it converges to $f (x)$ , so uniqueness of limits gives $f (x) = \sup_{k} f_{k} (x)$ ; hence $f_{k} (x) \leq f (x)$ for every $k \in N$ and every $x \in X$ .

step 1.1A2L2L3

2.2

Each $U_{k}$ is open: let $a \in U_{k}$ and put $η : = (ε - (f (a) - f_{k} (a))) / 2 > 0$ ; continuity of $f$ and of $f_{k}$ at $a$ gives reals $δ_{1}, δ_{2} > 0$ with $∣ f (x) - f (a) ∣ < η$ for $d (x, a) < δ_{1}$ and $∣ f_{k} (x) - f_{k} (a) ∣ < η$ for $d (x, a) < δ_{2}$ , and then $δ : = \min {δ_{1}, δ_{2}} > 0$ gives, for $d (x, a) < δ$ , the estimate $f (x) - f_{k} (x) < (f (a) + η) - (f_{k} (a) - η) = (f (a) - f_{k} (a)) + 2 η = ε$ , so $B (a, δ) \subseteq U_{k}$ .

step 1.2A2L4L5choose

2.3

$X = ⋃_{k \in N} U_{k}$ : given $x \in X$ , convergence $f_{k} (x) \to f (x)$ supplies $k$ with $∣ f_{k} (x) - f (x) ∣ < ε$ , hence $f (x) - f_{k} (x) < ε$ and $x \in U_{k}$ .

step 1.2A2

3.1

If $X = \emptyset$ the conclusion holds with $N : = 0$ , the condition being vacuous; so assume $X \neq \emptyset$ , and compactness applied to the family $(U_{k})_{k \in N}$ gives $n \in N$ and $k_{0}, \dots, k_{n} \in N$ with $X = U_{k_{0}} \cup \dots \cup U_{k_{n}}$ .

step 2.2step 2.3L6L8

4.1

By [L7] there is $j^{*} \leq n$ with $k_{j} \leq k_{j^{*}}$ for every $j \leq n$ ; put $N : = k_{j^{*}}$ .

step 3.1L7

5.1

$U_{m} \subseteq U_{N}$ whenever $m \leq N$ : for $x \in U_{m}$ we have $f_{m} (x) \leq f_{N} (x)$ by [L1], so $f (x) - f_{N} (x) \leq f (x) - f_{m} (x) < ε$ .

step 1.2step 4.1A1L1

6.1

Hence $X = U_{k_{0}} \cup \dots \cup U_{k_{n}} \subseteq U_{N}$ , so $X = U_{N}$ , that is $f (x) - f_{N} (x) < ε$ for every $x \in X$ .

step 3.1step 4.1step 5.1

7.1

For every $k \geq N$ and every $x \in X$ : $0 \leq f (x) - f_{k} (x) \leq f (x) - f_{N} (x) < ε$ , using $f_{k} (x) \leq f (x)$ from step 2.1 and $f_{N} (x) \leq f_{k} (x)$ from [L1]; so $∣ f_{k} (x) - f (x) ∣ < ε$ .

step 2.1step 6.1A1L1

8.1

As $ε$ was an arbitrary positive real, step 7.1 produces for each of them an index $N$ serving every point of $X$ , which is uniform convergence of $(f_{k})$ to $f$ .

step 1.2step 3.1step 7.1L8∎

Remarks

Where continuity of the limit is used. Only in step 2.2, to make $U_{k}$ open. Without it the sets $U_{k}$ need not be open, the cover argument collapses, and the conclusion is false: the companion page exhibits continuous $f_{k}$ increasing pointwise on the compact space $[0, 1]$ to a discontinuous limit, with no uniform convergence.
Where monotonicity is used. Twice, and both times to turn "some index works at this point" into "one index works at every point": at step 5.1, to make the sets $U_{k}$ increase with $k$ so that a finite subcover collapses to a single $U_{N}$ , and at step 7.1, to propagate the bound from $N$ to every later index.
Where compactness is used. Once, at step 3.1. On a non-compact domain the theorem fails, and the standard witness is the increasing sequence of functions on $(0, 1]$ that are $0$ up to $1 / (k + 1)$ and rise to $1$ ; nothing on this page needs that witness and it is not constructed here.
The conclusion is genuinely about the sequence and not about the family. Dini's theorem says nothing about an arbitrary set of continuous functions with a continuous pointwise supremum; the ordering of the sequence by its index is what steps 5.1 and 7.1 consume.

Depends on

Used by

Dini's theorem applied to a nondecreasing sequence of piecewise linear approximations on [0,1], and what fails when the limit is not continuous Example

Dependency tree · two levels

81 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

Dini's theorem (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 7 (standard reference, not scraped)