TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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 $R^{m}$ has Lebesgue outer measure zero if and only if it is null in the sense of countable closed-cube covers

Statement

Let $m \geq 1$ and assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). For $E \subseteq R^{m}$ ,

$λ_{m}^{*} (E) = 0 ⟺ E is null,$

nullity being the covering notion of Measure zero and content zero in $R^{m}$ by countable and finite cube covers: that is, if and only if for every real $ε > 0$ the set $E$ is covered by a sequence of closed cubes whose nonnegative volume series converges with sum at most $ε$ .

Facts & Assumptions

Given: A natural number $m \geq 1$ , the Axiom of Countable Choice, and a subset $E \subseteq R^{m}$ .

[L1]

Assuming countable choice, $λ^{c b} (E) = λ_{m}^{*} (E)$ , where $λ^{c b} (E)$ is the infimum of $\sum_{k = 0}^{\infty} ℓ_{k}^{m}$ over countable covers of $E$ by closed cubes $\prod_{i < m} [c_{i}^{k}, c_{i}^{k} + ℓ_{k}]$ (Countable covers by closed boxes, by open boxes and by closed cubes all compute Lebesgue outer measure, Lebesgue outer measure on $R^{n}$ ).

[F1]

A closed cube is a rectangle $\prod_{j < m} [a_{j}, a_{j} + ℓ]$ with $ℓ \geq 0$ ; its volume is $ℓ^{m}$ . A set $E \subseteq R^{m}$ is null when, for every $ε > 0$ , it is covered by a sequence of closed cubes whose nonnegative volume series converges with sum at most $ε$ (Measure zero and content zero in $R^{m}$ by countable and finite cube covers, Axis-parallel rectangles in $R^{m}$ and their volume).

[F2]

The nonnegative extended sum of a sequence in $[0, + \infty]$ is $\sum_{k = 0}^{\infty} a_{k} : = \sup_{n \in N} s_{n}$ , the supremum of its nondecreasing partial sums (Series in the nonnegative extended real line).

Proof

technique · direct

1.1

The closed cubes admitted in the published definition of nullity are exactly the sets $\prod_{i < m} [c_{i}, c_{i} + ℓ]$ with $ℓ \geq 0$ , with the same size $ℓ^{m}$ as in $λ^{c b}$ , so the two notions quantify over the same covers with the same terms.

1.2

For a sequence of nonnegative reals, the nonnegative extended sum is the supremum of the partial sums, so the condition that the volume series converges with sum at most $ε$ says exactly that this sum, taken in $[0, + \infty]$ , is at most $ε$ .

2.1

Hence $E$ is null in the published sense if and only if for every real $ε > 0$ some admissible cube cover has total volume at most $ε$ , which says exactly that the infimum $λ^{c b} (E)$ is $0$ ; and $λ^{c b} (E) = λ_{m}^{*} (E)$ .

step 1.1step 1.2L1∎

Depends on

Used by

Dependency tree · two levels

39 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)

A subset of RmRm has Lebesgue outer measure zero if and only if it is null in the sense of countable closed-cube covers