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 real function on a compact Jordan measurable set is Riemann integrable over that set
Statement
Every continuous real function on a compact Jordan measurable set is Riemann integrable over .
Facts & Assumptions
Given: Compact Jordan measurable and continuous .
A continuous real function on a nonempty compact metric space is bounded (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Lower bound, bounded below, bounded set).
The boundary of is null (A bounded set in is Jordan measurable iff its boundary is null, equivalently of content zero).
A bounded function on a rectangle is integrable exactly when its discontinuity set is null (Lebesgue's criterion in : a bounded function on a closed nondegenerate rectangle is Riemann integrable iff its discontinuity set is null).
Proof
If , its zero extension is identically zero and the conclusion is immediate. Otherwise [L1] makes bounded. Choose a bounding rectangle and form its zero extension as in The Riemann integral of a bounded function over a bounded Jordan measurable set.
The extension is continuous at every point of the interior of , by continuity of , and at every point outside the closure of , because it is locally zero. Its discontinuities are therefore contained in .
The containing boundary is null by [L2], so subset closure and [L3] make the extension integrable. Bounding-rectangle independence is The Riemann integral over a Jordan set is independent of the bounding rectangle.
Depends on
- The Riemann integral of a bounded function over a bounded Jordan measurable set
- The Riemann integral over a Jordan set is independent of the bounding rectangle
- A bounded set in $\mathbb{R}^m$ is Jordan measurable iff its boundary is null, equivalently of content zero
- Lebesgue's criterion in $\mathbb{R}^m$: a bounded function on a closed nondegenerate rectangle is Riemann integrable iff its discontinuity set is null
- Continuity of a map between metric spaces, at a point and globally, in the $\varepsilon$-$\delta$ form
- Interior, closure, boundary, limit point, isolated point and dense subset of a metric space
- Open cover, subcover, compact metric space, and compact subset of a metric space
- A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value
- Lower bound, bounded below, bounded set
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 140 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- J. Lebl, Basic Analysis, Jordan Measurable Sets (standard reference, not scraped)
- J. Lebl, Basic Analysis, Outer Measure and Null Sets (standard reference, not scraped)