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 subset of has Lebesgue outer measure zero if and only if it has measure zero in the sense of countable closed-interval covers
Statement
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()) and let . Then
measure zero being the covering notion of Measure zero (a countable cover by intervals of total length below every ) and content zero (a finite such cover): that is, if and only if for every real there are sequences and of reals with for every such that and converges with sum at most .
Facts & Assumptions
Given: The Axiom of Countable Choice, the case of Lebesgue outer measure, and a subset .
Assuming countable choice, , where is the infimum of over countable covers of by closed rectangles (Countable covers by closed boxes, by open boxes and by closed cubes all compute Lebesgue outer measure, Lebesgue outer measure on ).
has measure zero, equivalently is null, when for every real there are sequences and of reals with for every , such that and converges with sum (Measure zero (a countable cover by intervals of total length below every ) and content zero (a finite such cover), Intervals of : the nine order-convex forms, nondegeneracy, and length).
For a fixed , converges with sum if and only if for every (Measure zero (a countable cover by intervals of total length below every ) and content zero (a finite such cover)).
The nonnegative extended sum of a sequence in is , the supremum of its nondecreasing partial sums (Series in the nonnegative extended real line).
Under the standard identification , the rectangle of is the interval and its volume is its length (Axis-parallel rectangles in and their volume).
Proof
At a closed rectangle is a closed interval with and its volume is the length , so the covers admitted in are exactly the covers admitted in the published definition of measure zero.
For a sequence of nonnegative reals, the nonnegative extended sum is the supremum of the partial sums, so it is at most exactly when every partial sum is, which is exactly the condition that the real series converges with sum at most .
Hence has measure zero in the published sense if and only if for every real some admissible cover has total length at most , which says exactly that the infimum is ; and .
Depends on
- Countable covers by closed boxes, by open boxes and by closed cubes all compute Lebesgue outer measure
- Measure zero (a countable cover by intervals of total length below every $\varepsilon$) and content zero (a finite such cover)
- Lebesgue outer measure on $\mathbb{R}^n$
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Series in the nonnegative extended real line
- Axis-parallel rectangles in $\mathbb{R}^m$ and their volume
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
- A bounded function on a closed bounded interval, or on a closed nondegenerate rectangle, is Riemann integrable exactly when its discontinuity set has Lebesgue measure zero Corollary
- A property holding outside a set of elementary measure zero is exactly a property holding λ-almost everywhere Corollary
- The Cantor set is an uncountable subset of ℝ of Lebesgue measure zero Corollary
- A Lebesgue measurable subset of ℝ with empty interior has measure zero False statement
- The published refutations separating nullity from nowhere density hold verbatim for Lebesgue measure Remark
Dependency tree · two levels
42 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
- John K. Hunter, Measure Theory (UC Davis lecture notes), Chapter 2 (standard reference, not scraped)
- T. Tao, An Introduction to Measure Theory (GSM 126), Section 1.2 (standard reference, not scraped)