TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-11

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 region between two continuous graphs is Jordan measurable, and a continuous integrand extending to its closure integrates by vertical sections

Statement

Let $a < b$ , let $α, β : [a, b] \to R$ be continuous with $α \leq β$ , and put $K : = {(x, y) : a \leq x \leq b, α (x) \leq y \leq β (x)} .$ Then $K$ is compact and Jordan measurable. If a function on the open region between the graphs extends to a continuous $H : K \to R$ , then $H$ is Riemann integrable over $K$ and $\int_{K} H = \int_{a}^{b} (\int_{α (x)}^{β (x)} H (x, y) d y) d x .$ The formula includes coincident graphs and uses the continuous extension on the boundary.

Facts & Assumptions

Given: Continuous $α \leq β$ on $[a, b]$ , the closed region $K$ , and a continuous $H : K \to R$ .

[L1]

Jordan--Fubini integrates a bounded integrable function over a Jordan set by its Jordan sections (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable).

[L2]

A metric-bounded set is Jordan measurable if and only if its boundary is null, equivalently content zero (A bounded set in $R^{m}$ is Jordan measurable iff its boundary is null, equivalently of content zero).

[L3]

The graph of a continuous real function on a compact Jordan domain has content zero (The graph of a continuous function on a closed nondegenerate rectangle in $R^{m}$ has content zero in $R^{m + 1}$ ).

[L4]

A continuous real function on a compact Jordan set is Riemann integrable there (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set).

[L5]

A closed bounded subset of $R^{2}$ is compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

Proof

technique · direct

1.1

The boundary of $K$ is contained in the graphs of $α$ and $β$ together with the two vertical endpoint segments. Each is a continuous graph, after exchanging coordinates for the vertical segments, and hence has content zero by [L3]. The set $K$ is closed and bounded, hence compact by [L5], and [L2] makes it Jordan measurable.

L2L3L5given

2.1

The continuous $H$ is integrable on the compact Jordan set by [L4]. Every vertical section is the closed interval $[α (x), β (x)]$ , and its restriction is continuous, so [L1] gives the displayed formula.

L1L4step 1.1

3.1

If $α (x) = β (x)$ , that section is degenerate and contributes $0$ ; the endpoint sections and all other boundary changes have content zero. Requiring a continuous extension to $K$ supplies boundedness and integrability that continuity only on the open region would not supply.

step 2.1algebra∎

Depends on

Used by

Type I, Type II, and elementary regions for Green's theorem Definition
The Type I boundary identity for the P dx term Lemma
The Type II boundary identity for the Q dy term Lemma
Riemann area between continuous graphs equals Jordan content Proposition

Dependency tree · two levels

51 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 II, Proposition 10.5.8 and Exercise 10.5.3 (standard reference, not scraped)
A. Leibman, Multidimensional Real Analysis, §5.4 (standard reference, not scraped)