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 is Lebesgue null in
Example
Assume the Axiom of Countable Choice and let be continuous. Then its graph
is Lebesgue null in .
Facts & Assumptions
Given: The Axiom of Countable Choice and a continuous function .
A subset of has Lebesgue outer measure zero if and only if it is null in the sense of countable closed-cube covers (A subset of has Lebesgue outer measure zero if and only if it is null in the sense of countable closed-cube covers).
Assuming countable choice, a box in with parameters is Lebesgue measurable of measure (A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included).
Let be a measure and let be measurable. Then (Finite and countable subadditivity of measures).
Then is continuous at when every neighbourhood of contains the image of some neighbourhood of (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
A subset is compact exactly when it is closed and bounded (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).
A continuous real function on a compact subset of is uniformly continuous (Heine-Cantor in : a continuous real function on a compact subset of is uniformly continuous, proved -natively from sequential compactness).
For every real there is a natural number with (For every in a complete ordered field there is a natural with ).
If then the series converges; in particular (For , , and for the series diverges).
Verification
Fix a real . For each integer , the interval is compact by [F3], so [L3] gives a real such that and imply . By [F4] choose a natural number with , and put for . Then for every with and every one has , hence .
For each such subinterval, the corresponding graph piece lies in the closed box , whose width is and whose height is . Therefore [L2] gives a box cover of whose total area is .
Summing these covers over all integers and using [F1], the whole graph is covered by countably many closed boxes with total area at most , the geometric-series identity coming from [F5]. Since was arbitrary, [L1] gives that is Lebesgue null.
Depends on
- A subset of $\mathbb{R}^m$ has Lebesgue outer measure zero if and only if it is null in the sense of countable closed-cube covers
- A box in $\mathbb{R}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure $\prod_{i<n}(b_i-a_i)$, whichever of its faces are included
- Finite and countable subadditivity of measures
- Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$: the $\varepsilon$-$\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point
- Heine-Cantor in $\mathbb{R}$: a continuous real function on a compact subset of $\mathbb{R}$ is uniformly continuous, proved $\mathbb{R}$-natively from sequential compactness
- 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
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- For $|r| < 1$, $\sum_{k \ge 0} r^k = 1/(1-r)$, and for $|r| \ge 1$ the series diverges
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
76 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
- T. Tao, An Introduction to Measure Theory (GSM 126), Exercise 1.1.7 (standard reference, not scraped)