TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-07-31

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 closed interval: monotone pointwise convergence of continuous functions to a continuous limit is uniform

Statement

Let $a < b$ be reals. Suppose $f_{k} : [a, b] \to R$ and $f : [a, b] \to R$ are continuous, $f_{k} \to f$ pointwise, and the sequence is pointwise monotone in one fixed direction:

$f_{k} (x) \leq f_{k + 1} (x) for all k, x,$

$f_{k + 1} (x) \leq f_{k} (x) for all k, x .$

Then $f_{k} \to f$ uniformly on $[a, b]$ .

Facts & Assumptions

Given: Reals $a < b$ , continuous functions $f_{k}, f : [a, b] \to R$ , pointwise convergence $f_{k} \to f$ , and one of the two pointwise monotonicity conditions in the Statement.

[A1]

Uniform convergence means that for every real $ε > 0$ there is $N$ such that $∣ f_{k} (x) - f (x) ∣ < ε$ for every $k \geq N$ and every $x \in [a, b]$ (Pointwise convergence, uniform convergence, and the uniformly Cauchy condition for sequences of real-valued functions).

[L1]

Sums and scalar multiples of continuous real functions are continuous (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

[L2]

If $h : A \to R$ is continuous, the inverse image of an open subset of $R$ is relatively open in $A$ : it is $O \cap A$ for some open $O \subseteq R$ ( $f : A \to R$ is continuous on $A$ if and only if the preimage of every open subset of $R$ is the intersection with $A$ of an open subset of $R$ , and dually for closed sets).

[L3]

Every open cover of the closed bounded interval $[a, b]$ has a finite subcover (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact).

[L4]

Every finite list of natural numbers has a greatest member: apply the finite-real maximum theorem to their canonical images, which preserve the natural-number order; finite choices can be made without any choice axiom (Every nonempty finite set of reals has a maximum and a minimum, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing, $\leq$ is a linear order on $N$ , Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

Proof

technique · direct

1.1

Fix a real $ε > 0$ . For each $n \in N$ put $h_{n} : = f_{n} - f$ and $U_{n} : = {x \in [a, b] : ∣ h_{n} (x) ∣ < ε}$ . The function $h_{n}$ is continuous by [L1], so [L2] makes $U_{n}$ relatively open in $[a, b]$ .

L1L2construct

1.2

In the nondecreasing case, pointwise convergence forces $f_{n} (x) \leq f (x)$ for every $n, x$ , and the errors $f (x) - f_{n} (x)$ decrease with $n$ ; in the nonincreasing case it forces $f (x) \leq f_{n} (x)$ and the errors $f_{n} (x) - f (x)$ decrease. Thus $U_{n} \subseteq U_{n + 1}$ in either case, and pointwise convergence gives $⋃_{n} U_{n} = [a, b]$ .

givenalgebra

2.1

Let $O$ be the family of all open sets $O \subseteq R$ whose trace $O \cap [a, b]$ equals $U_{n}$ for some $n$ . By step 1.1 each $U_{n}$ has such an open witness, and by step 1.2 the family $O$ covers $[a, b]$ .

step 1.1step 1.2L2construct

3.1

By [L3], choose finitely many $O_{0}, \dots, O_{r} \in O$ covering $[a, b]$ . By finite choice, choose $n_{0}, \dots, n_{r}$ with $O_{i} \cap [a, b] = U_{n_{i}}$ , and let $N : = \max {n_{0}, \dots, n_{r}}$ .

step 2.1L3L4choose

4.1

Since the $U_{n}$ are increasing, every $U_{n_{i}}$ is contained in $U_{N}$ ; the traces of the $O_{i}$ cover $[a, b]$ , so $U_{N} = [a, b]$ , and then $U_{k} = [a, b]$ for every $k \geq N$ .

step 1.2step 3.1

5.1

Therefore $∣ f_{k} (x) - f (x) ∣ < ε$ for every $k \geq N$ and every $x \in [a, b]$ . Since $ε$ was arbitrary, the convergence is uniform.

step 4.1A1∎

Depends on

Used by

Dependency tree · two levels

49 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

J. Lebl, Basic Analysis I, §6.1 (standard reference, not scraped)
Dini's theorem (Wikipedia) (standard reference, not scraped)
W. Trench, Introduction to Real Analysis (standard reference, not scraped)