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.
The graph of a continuous function on a closed nondegenerate rectangle in has content zero in
Statement
Let , let be a closed nondegenerate rectangle, and let be continuous. Its graph has content zero in .
Facts & Assumptions
Given: as stated.
is compact and uniformly continuous (Heine-Borel in : with the Euclidean metric a subset of 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, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous, Continuity of a map between metric spaces, at a point and globally, in the - form).
Grid cells and cube volumes are Grid partitions of a rectangle in , their cells, refinements and mesh and Axis-parallel rectangles in and their volume.
Proof
Given , choose a uniform coordinate grid with cell widths at most , where uniform continuity makes the oscillation of on each cell below a vertical amount . Since is nondegenerate, the grid may be chosen so that the number of cells satisfies for a constant depending only on .
One horizontal cube footprint of side covers each domain cell. Above it, stack -cubes of side across the graph's vertical range. Integer part: for every real there is exactly one integer with bounds their number by , so all stacks together have volume at most .
Summing over the finitely many domain cells gives total covering volume at most a rectangle-dependent constant times . Choose and then to make this below .
This finite cube cover proves content zero in the sense of Measure zero and content zero in by countable and finite cube covers.
Depends on
- Measure zero and content zero in $\mathbb{R}^m$ by countable and finite cube covers
- Grid partitions of a rectangle in $\mathbb{R}^m$, their cells, refinements and mesh
- Axis-parallel rectangles in $\mathbb{R}^m$ and their volume
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{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
- Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous
- Continuity of a map between metric spaces, at a point and globally, in the $\varepsilon$-$\delta$ form
- Each $\lVert\cdot\rVert_p$ is a norm on $\mathbb{R}^n$, and the induced metrics are exactly $d_1$, $d_2$ and $d_\infty$ of the published metric-spaces page
- Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Laws of finite sums and finite products
Used by
- The parabola segment {(x,x²):0≤ x≤1} has content zero in ℝ² Example
- The right triangle {(x,y)∈[0,1]²:x+y≤1} has Jordan content 1/2 Example
- A compact subset of an open Euclidean set has a compact Jordan neighborhood inside that open set Lemma
- Conventions and proved scope for the Riemann integral in ℝᵐ and Jordan content Remark
- A region between two continuous graphs is Jordan measurable, and a continuous integrand extending to its closure integrates by vertical sections Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 174 results over 28 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)
- A. Cañez, multivariable calculus notes (standard reference, not scraped)