TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-24

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 solid between continuous graphs over a compact Jordan base is Jordan measurable and integrates by vertical sections

Statement

Let $D \subseteq R^{m}$ be compact and Jordan measurable, let $α, β : D \to R$ be continuous with $α \leq β$ , and put $K : = {(u, t) : u \in D, α (u) \leq t \leq β (u)}$ . The solid $K$ is compact and Jordan measurable, and every continuous $H : K \to R$ satisfies $\int_{K} H = \int_{D} (\int_{α (u)}^{β (u)} H (u, t) d t) d u$ .

Facts & Assumptions

Given: The data in the Statement, with integrals understood in the multidimensional Riemann sense.

[F1]

The boundary of $K$ has content zero (The boundary of a solid between continuous graphs over a compact Jordan base has content zero).

[F2]

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

[F3]

If $E \subseteq R^{p + q}$ is bounded Jordan, $g : E \to R$ is integrable, and outside a content-zero parameter set the sections $E_{x}$ are Jordan measurable and the restrictions $g_{x}$ are integrable, then the completed section-integral function is integrable and $\int_{E} g = \int (\int_{E_{x}} g_{x}) d x$ ; the symmetric coordinate order also holds (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable).

[F4]

Continuous real functions on a nonempty compact metric space attain finite extrema and are bounded (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F5]

A Euclidean set is compact if and only if it is closed and bounded (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

If $D = \emptyset$ , every assertion and both integrals are zero. Otherwise [F4] bounds $α$ and $β$ ; the defining weak inequalities make $K$ closed, so it is closed and bounded and therefore compact by [F5].

givenF4F5algebra

2.1

By [F1] the boundary of the bounded set $K$ has content zero, so the Jordan boundary criterion makes $K$ Jordan measurable.

step 1.1F1

3.1

By [F2], $H$ is integrable on $K$ . For each $u \in D$ , the vertical section is exactly $[α (u), β (u)]$ , and the restriction $t \mapsto H (u, t)$ is continuous and integrable; [F3] therefore gives the displayed iterated formula.

step 2.1F2F3

4.1

If $α (u) = β (u)$ , the corresponding section is a singleton and its integral is zero. Thus coincident graphs, whether at isolated points or everywhere, require no exceptional convention.

step 3.1algebra∎

Depends on

Used by

Dependency tree · two levels

54 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

Michael E. Taylor, Introduction to Analysis in Several Variables, Theorem 3.1.9 (standard reference, not scraped)