TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck pass

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.

Statement references

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

Lower bound, bounded below, bounded set

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$

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, 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.1givenL1L3L4L7L8L9choose

$[a, b]$ is compact by [L1], so [L3] supplies uniform continuity. Apply it with tolerance $1$ and fix $δ_{0} > 0$ such that $∣ f (x) - f (y) ∣ < 1$ whenever $x, y \in [a, b]$ and $∣ x - y ∣ < δ_{0}$ . By [L7], choose $N_{0} \geq 1$ with $(b - a) / ι (N_{0}) < δ_{0}$ , and take the uniform partition with nodes $t_{0} = a, \dots, t_{N_{0}} = b$ . Adjacent nodes have distance less than $δ_{0}$ , so $∣ f (t_{j + 1}) - f (t_{j}) ∣ < 1$ . Telescoping the inequalities $- 1 < f (t_{j + 1}) - f (t_{j}) < 1$ and using the absolute-value bounds give $∣ f (t_{i}) ∣ \leq ∣ f (a) ∣ + ι (i)$ for every $i \leq N_{0}$ . Every $x \in [a, b]$ lies in some $[t_{i}, t_{i + 1}]$ , with $i < N_{0}$ , and has $∣ x - t_{i} ∣ < δ_{0}$ ; hence $f (t_{i}) - 1 < f (x) < f (t_{i}) + 1$ and therefore $∣ f (x) ∣ < ∣ f (a) ∣ + ι (N_{0}) + 1$ . Thus $f$ is bounded and its Darboux sums and integrals are defined. Compactness has been used only to obtain uniform continuity.

1.2givenL9

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

2.1step 1.1step 1.2L1L3choose

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 ∣ < δ$ .

3.1step 2.1L4L7L9choose

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].

4.1step 2.1step 3.1L5L9

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].

5.1step 4.1L4L5L8L9

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].

6.1step 1.1step 1.2step 5.1L6∎

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.

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] to apply Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous and get uniform continuity on the whole interval. Step 1.1 derives boundedness from this uniform continuity by a finite uniform mesh, so no separate compactness argument is needed for boundedness. On a non-compact interval both uniform continuity and boundedness can fail: $x \mapsto 1 / x$ is continuous on $(0, 1)$ and unbounded there, so it has no Darboux sums at all.
Choice. The proof selects nothing from an infinite family. The current proof of Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous also uses only a finite subcover, so this integrability argument is choice-free. See Choice ledger for the Riemann integral: the page results are proved in ZF.

Depends on

Dependency tree · 2 levels

Sources

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

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