LemmaStatement: Literature-sourcedProof: 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.

A function integrable on $[a, b]$ is integrable on every closed subinterval

Statement

Let $a < b$ be reals, let $f : [a, b] \to R$ be integrable (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$ ), and let $c, d$ satisfy

$a \leq c < d \leq b .$

Then the restriction of $f$ to $[c, d]$ is bounded (Lower bound, bounded below, bounded set) and integrable on $[c, d]$ .

The degenerate case $c = d$ is not an omission: there $\int_{c}^{c} f = 0$ by The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , and no partition of $[c, d]$ exists to speak of (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).

Facts & Assumptions

Given: Reals $a < b$ , an integrable $f : [a, b] \to R$ , and reals $c, d$ with $a \leq c < d \leq b$ . Write $g$ for the restriction of $f$ to $[c, d]$ .

[L1]

Riemann's criterion: a bounded function on a closed bounded interval with distinct endpoints is integrable if and only if for every real $ε > 0$ there is a partition $P$ of that interval with $U (\cdot, P) - L (\cdot, 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) < ε$ , 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$ ).

[L2]

For a partition $P$ of $[a, b]$ and a point $p \in [a, b]$ , the partition $P + p$ satisfies $pts (P + p) = pts (P) \cup {p}$ and refines $P$ ; a refinement of a refinement refines the original, since the point-set inclusions compose (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).

[L3]

If $P^{'}$ refines $P$ then $L (f, P) \leq L (f, P^{'}) \leq U (f, P^{'}) \leq U (f, P)$ (Refining a partition raises the lower Darboux sum and lowers the upper one, and every lower sum is at most every upper sum: $L (f, P) \leq L (f, P^{'}) \leq U (f, P^{'}) \leq U (f, P)$ when $P^{'}$ refines $P$ , and $L (f, P) \leq U (f, Q)$ for arbitrary partitions $P$ and $Q$ ; moreover the two changes are at most $2 M (n^{'} - n) ∥ P ∥$ , claim 1).

[L4]

For a partition $R = (n, t)$ of an interval and bounded $h$ on it: $L (h, R) = \sum_{i < n} m_{i} Δ_{i}$ , $U (h, R) = \sum_{i < n} M_{i} Δ_{i}$ with $m_{i} = \inf h [I_{i}]$ , $M_{i} = \sup h [I_{i}]$ , $I_{i} = [t_{i}, t_{i + 1}]$ , $Δ_{i} = t_{i + 1} - t_{i} > 0$ , and $M_{i} - m_{i} \geq 0$ (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}$ , 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, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L5]

Finite sums: additivity, scaling, splitting at an intermediate index with $\sum_{k = m}^{n - 1} a_{k} = \sum_{j < n - m} a_{m + j}$ , and monotonicity in the terms, so that a sum of nonnegative terms is at most a sum containing those terms among others (Finite sums and finite products, by recursion, Laws of finite sums and finite products, clauses 1 to 4).

[L6]

A partition $P^{'} = (n^{'}, t^{'})$ of $[a, b]$ has $t^{'}$ strictly increasing on indices $\leq n^{'}$ , hence injective there, so a point of $pts (P^{'})$ is $t_{j}^{'}$ for exactly one $j \leq n^{'}$ ; and $j < k$ gives $t_{j}^{'} < t_{k}^{'}$ (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).

[L7]

A restriction of a bounded function is bounded: the same $M$ serves fewer points (Lower bound, bounded below, bounded set).

Proof

technique · direct

1.1givenL7

$g$ is bounded on $[c, d]$ , since $[c, d] \subseteq [a, b]$ and $f$ is bounded on $[a, b]$ , integrability presupposing boundedness.

1.2givenL1choose

Let a real $ε > 0$ be given, and fix a partition $P$ of $[a, b]$ with $U (f, P) - L (f, P) < ε$ .

2.1step 1.2L2construct

Put $P^{'} : = (P + c) + d$ , a partition of $[a, b]$ refining $P$ whose point set contains $c$ and $d$ .

3.1step 1.2step 2.1L3

By [L3] applied to the pair $(P, P^{'})$ , $U (f, P^{'}) - L (f, P^{'}) \leq U (f, P) - L (f, P) < ε$ .

3.2step 2.1L6choose

Write $P^{'} = (n^{'}, t^{'})$ and fix the unique indices $p, q \leq n^{'}$ with $t_{p}^{'} = c$ and $t_{q}^{'} = d$ ; then $p < q$ , because $c < d$ and $t^{'}$ is increasing on those indices.

4.1step 3.2L6construct

Define $Q : = (q - p, s)$ by $s_{i} : = t_{p + i}^{'}$ for $i \leq q - p$ and $s_{k} : = d$ for $k \geq q - p$ . Then $s_{0} = t_{p}^{'} = c$ , $s_{q - p} = t_{q}^{'} = d$ , and $s_{i} < s_{i + 1}$ for $i < q - p$ by [L6], with $q - p \geq 1$ ; so $Q$ is a partition of $[c, d]$ , its $i$ -th subinterval is $[t_{p + i}^{'}, t_{p + i + 1}^{'}] = I_{p + i}^{'}$ and its $i$ -th length is $Δ_{p + i}^{'}$ .

5.1step 4.1L4L5

For $i < q - p$ the $i$ -th subinterval of $Q$ is $I_{p + i}^{'} \subseteq [c, d]$ , and $g$ agrees with $f$ there, so the extreme values of $g$ on it are $M_{p + i}^{'}$ and $m_{p + i}^{'}$ ; hence $U (g, Q) - L (g, Q) = \sum_{i < q - p} (M_{p + i}^{'} - m_{p + i}^{'}) Δ_{p + i}^{'}$ by [L4] and [L5].

6.1step 5.1L4L5

Every term $(M_{j}^{'} - m_{j}^{'}) Δ_{j}^{'}$ is nonnegative by [L4], and splitting $\sum_{j < n^{'}}$ first at $p$ and then at $q$ exhibits $\sum_{i < q - p} (M_{p + i}^{'} - m_{p + i}^{'}) Δ_{p + i}^{'}$ as one of the three pieces of $\sum_{j < n^{'}} (M_{j}^{'} - m_{j}^{'}) Δ_{j}^{'}$ , the other two being nonnegative; so the displayed sum is at most $U (f, P^{'}) - L (f, P^{'})$ .

7.1step 3.1step 5.1step 6.1

Combining, $U (g, Q) - L (g, Q) \leq U (f, P^{'}) - L (f, P^{'}) < ε$ .

8.1step 1.1step 1.2step 7.1L1∎

Since $ε > 0$ was arbitrary and $g$ is bounded, [L1] applies on $[c, d]$ and $g$ is integrable there.

Remarks

The one step that is not bookkeeping is the re-indexing. A partition in this library is a pair $(n, t)$ with a tail convention (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), not a set of points, so "restrict $P^{'}$ to $[c, d]$ " is not a defined operation; step 4.1 writes the restricted list out, shifts its index by $p$ and resets its tail to $d$ . Everything else follows from the fact that dropping nonnegative terms from a finite sum cannot increase it.
The converse is also true, and is proved separately. Integrability on $[a, c]$ and on $[c, b]$ gives integrability on $[a, b]$ ; that direction needs a splice rather than a restriction and is the second half of For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ .

A function integrable on $[a, b]$ is integrable on every closed subinterval

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

A function integrable on [a,b][a,b] is integrable on every closed subinterval

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

A function integrable on $[a, b]$ is integrable on every closed subinterval