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 $\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
- Green's second identity on a glued elementary solid region Corollary
- The divergence at a point is the limit of outward flux per unit volume Corollary
- The normal component of the curl is the limiting circulation per unit area of shrinking discs Corollary
- Integral of a form over a smooth singular simplex Definition
- Surface area and scalar surface integrals on a regular patch Definition
- Both sides of the divergence theorem for F(x,y,z)=(x²,y²,z²) on the closed unit box Example
- Change of variables for a C¹ map injective and regular only on the interior of a compact Jordan set Lemma
- Integration over the signed shuffle equals the product of simplex integrals Lemma
- Internal faces cancel and volume integrals add when elementary solid regions are glued Lemma
- Riemann–Lebesgue comparison for distribution test integrands Lemma
- Stokes theorem for the standard simplex Lemma
- The flux of a single-component field through a graph face is a base integral of its trace Lemma
- The plane Gaussian integral equals π by polar coordinates Lemma
- The single-direction flux identity on a simple solid region Lemma
- The Type II boundary identity for the Q dy term Lemma
- A region between two continuous graphs is Jordan measurable, and a continuous integrand extending to its closure integrates by vertical sections Theorem
- A solid between continuous graphs over a compact Jordan base is Jordan measurable and integrates by vertical sections Theorem
- Change of variables for an injective C¹ map on a compact Jordan set Theorem
- Locally dominated parameter-dependent improper multiple integrals are continuous Theorem
- The divergence theorem on an elementary solid region Theorem
Dependency tree · two levels
52 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, Jordan Measurable Sets (standard reference, not scraped)
- J. Lebl, Basic Analysis, Outer Measure and Null Sets (standard reference, not scraped)