Alphabeta MathHow 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 is Jordan measurable iff its boundary is null, equivalently of content zero
Lebesgue's criterion in : 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 - 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