TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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 continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion

Statement

Let $a < b$ be reals and let $f : [a, b] \to R$ be continuous on $[a, b]$ (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). Then $f$ is bounded (Lower bound, bounded below, bounded set) and Riemann integrable on $[a, b]$ (The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ ).

The proof gives more than integrability: it gives a partition that works. For every real $ε > 0$ the uniform partition into $N$ parts already satisfies $U (f, P) - L (f, P) < ε$ , as soon as $N$ is large enough that $(b - a) / ι (N)$ is below the $δ$ that uniform continuity supplies for $ε / (2 (b - a))$ . Uniform continuity is exactly what makes one $δ$ serve all $N$ subintervals at once, and it is the only place where the compactness of $[a, b]$ is used.

Facts & Assumptions

Given: Reals $a < b$ and a function $f : [a, b] \to R$ continuous on $[a, b]$ .

[L1]

$[a, b]$ is closed and bounded, hence compact (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Open subset of $R$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen, Lower bound, bounded below, bounded set, A subset of $R$ is compact if and only if it is closed and bounded, Open cover, subcover, compact subset of $R$ (every open cover has a finite subcover), and sequentially compact subset).

[L2]

A continuous real function on a compact subset of $R$ is bounded there (A continuous real function on a compact subset of $R$ is bounded).

[L3]

Heine-Cantor: a continuous real function on a compact subset $K$ of $R$ is uniformly continuous on $K$ , that is, for every real $η > 0$ there is a real $δ > 0$ with $∣ f (x) - f (y) ∣ < η$ for all $x, y \in K$ with $∣ x - y ∣ < δ$ (Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous, proved $R$ -natively from sequential compactness, Uniform continuity of $f : A \to R$ : one $δ$ serving every pair of points of $A$ ).

[L4]

For a partition $P = (n, t)$ of $[a, b]$ : $Δ_{i} = t_{i + 1} - t_{i} > 0$ , $\sum_{i < n} Δ_{i} = b - a$ , and the uniform partition $U_{N}$ into $N \geq 1$ parts has every $Δ_{i}$ equal to $(b - a) / ι (N)$ (Partition of $[a, b]$ as a finite strictly increasing list $a = t_{0} < t_{1} < \dots < t_{n} = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions).

[L5]

$U (f, P) - L (f, P) = \sum_{i < n} (M_{i} - m_{i}) Δ_{i}$ and $M_{i} - m_{i} = \sup {∣ f (x) - f (y) ∣ : x, y \in I_{i}}$ for bounded $f$ (For bounded $f$ on $[a, b]$ and a partition $P$ : the infimum $m_{i}$ and supremum $M_{i}$ of $f$ on the $i$ -th subinterval, and the lower and upper Darboux sums $L (f, P) = \sum_{i} m_{i} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{i}$ , Laws of finite sums and finite products).

[L6]

Riemann's criterion: a bounded $f$ is integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ (Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ ).

[L7]

For every real $η > 0$ there is a natural $N \geq 1$ with $1 / ι (N) < η$ , and $ι (N) > 0$ for $N \geq 1$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Every complete ordered field is Archimedean, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing).

[L8]

Finite sums: scaling and monotonicity in the terms (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L9]

Ordered-field arithmetic and the absolute value: adding a constant and multiplying by a positive quantity preserve an inequality; the order is total and transitive; $x, y \in [c, d]$ gives $∣ x - y ∣ \leq d - c$ (Basic properties of the absolute value, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property), Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.

Proof

technique · direct

1.1

$[a, b]$ is compact by [L1], so $f$ is bounded on $[a, b]$ by [L2] and its Darboux sums and integrals are defined.

givenL1L2

1.2

Let a real $ε > 0$ be given and put $η : = ε \cdot (2 (b - a))^{- 1}$ , a positive real by [L9] since $b - a > 0$ .

givenL9

2.1

By [L3] applied to the compact set $[a, b]$ with this $η$ , fix a real $δ > 0$ such that $∣ f (x) - f (y) ∣ < η$ for all $x, y \in [a, b]$ with $∣ x - y ∣ < δ$ .

step 1.1step 1.2L1L3choose

3.1

By [L7] fix a natural $N \geq 1$ with $1 / ι (N) < δ \cdot (b - a)^{- 1}$ , and put $P : = U_{N} = (N, t)$ , the uniform partition of $[a, b]$ into $N$ parts. Then every $Δ_{i}$ equals $(b - a) / ι (N) < δ$ by [L4] and [L9].

step 2.1L4L7L9choose

4.1

For each $i < N$ and all $x, y \in I_{i} = [t_{i}, t_{i + 1}]$ one has $∣ x - y ∣ \leq Δ_{i} < δ$ by [L9], hence $∣ f (x) - f (y) ∣ < η$ by step 2.1. So $η$ is an upper bound of the set ${∣ f (x) - f (y) ∣ : x, y \in I_{i}}$ , and therefore $M_{i} - m_{i} \leq η$ by [L5].

step 2.1step 3.1L5L9

5.1

Consequently $U (f, P) - L (f, P) = \sum_{i < N} (M_{i} - m_{i}) Δ_{i} \leq \sum_{i < N} η Δ_{i} = η (b - a) = ε \cdot 2^{- 1} < ε$ , using [L5], step 4.1, $Δ_{i} > 0$ , [L8], [L4] and [L9].

step 4.1L4L5L8L9

6.1

Since the real $ε > 0$ of step 1.2 was arbitrary and step 5.1 produced a partition with $U (f, P) - L (f, P) < ε$ , criterion [L6] applies and $f$ is Riemann integrable on $[a, b]$ ; it is bounded by step 1.1.

step 1.1step 1.2step 5.1L6∎

Remarks

Continuity is sufficient and very far from necessary. A monotone function may have infinitely many discontinuities and is still integrable (A monotone function on $[a, b]$ is Riemann integrable: for the uniform partition into $N$ parts the upper minus lower sum telescopes to $∣ f (b) - f (a) ∣ (b - a) / ι (N)$ ); Thomae's function is discontinuous at every rational and integrable (A bounded function on $[a, b]$ whose set of discontinuities is at most countable is Riemann integrable); and the indicator of the Cantor set is discontinuous at uncountably many points and integrable. The exact frontier is Lebesgue's criterion for Riemann integrability: a bounded $f$ on $[a, b]$ is Riemann integrable if and only if its set of discontinuities has measure zero.
Where compactness enters, and what it buys. Only through [L1], and then twice: A continuous real function on a compact subset of $R$ is bounded to know that the Darboux sums exist at all, and Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous, proved $R$ -natively from sequential compactness to get one $δ$ for the whole interval. On a non-compact interval both can fail: $x \mapsto 1 / x$ is continuous on $(0, 1)$ and unbounded there, so it has no Darboux sums at all.
The choice cost is inherited, not incurred. Nothing in the proof above selects anything from an infinite family; the single use of countable choice behind this theorem sits inside Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous, proved $R$ -natively from sequential compactness, which names it in its own statement. See What this page costs in choice: Riemann's criterion, the Darboux-Riemann equivalence and integrability of a monotone function are theorems of ZF; integrability of a continuous function inherits the single use of countable choice inside Heine-Cantor; and only the forward half of the Lebesgue criterion spends countable choice, once, at the countable union of null sets.

Depends on

Used by

…and 19 more results.

Dependency tree · two levels

64 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

Riemann integral (Wikipedia) (standard reference, not scraped)
Heine-Cantor theorem (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 6 (standard reference, not scraped)
J. Lebl, Basic Analysis I, The Riemann Integral (standard reference, not scraped)
J. Hunter, Chapter 11: The Riemann Integral (standard reference, not scraped)

A continuous function on [a,b][a,b] is Riemann integrable, by Heine-Cantor and Riemann's criterion