Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck 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 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 (ACω)) and let A⊆R. Then

λ1∗(A)=0⟺A has measure zero,

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 ε>0 there are sequences (ak)k∈N and (bk)k∈N of reals with ak≤bk for every k such that A⊆⋃k∈N[ak,bk] and ∑k=0∞(bk−ak) converges with sum at most ε.

Facts & Assumptions

Given: The Axiom of Countable Choice, the case n=1 of Lebesgue outer measure, and a subset A⊆R.

[L1]

Assuming countable choice, λcl(E)=λn∗(E), where λcl(E) is the infimum of ∑k=0∞vol⁡[uk,vk] over countable covers of E by closed rectangles (Countable covers by closed boxes, by open boxes and by closed cubes all compute Lebesgue outer measure, Lebesgue outer measure on Rn).

[F1]

A has measure zero, equivalently A is null, when for every real ε>0 there are sequences (ak)k≥0 and (bk)k≥0 of reals with ak≤bk for every k≥0, such that A⊆⋃k≥0[ak,bk] and ∑k=0∞(bk−ak) converges with sum ≤ε (Measure zero (a countable cover by intervals of total length below every ε) and content zero (a finite such cover), Intervals of R: the nine order-convex forms, nondegeneracy, and length).

[F2]

For a fixed ε>0, ∑k=0∞(bk−ak) converges with sum ≤ε if and only if ∑k<n(bk−ak)≤ε for every n∈N (Measure zero (a countable cover by intervals of total length below every ε) and content zero (a finite such cover)).

[F3]

The nonnegative extended sum of a sequence in [0,+∞] is ∑k=0∞ak:=sup⁡n∈Nsn, the supremum of its nondecreasing partial sums (Series in the nonnegative extended real line).

[F4]

Under the standard identification R1≅R, the rectangle [a,b] of R1 is the interval [a0,b0] and its volume is its length (Axis-parallel rectangles in Rm and their volume).

Proof

technique · direct
1.1F1F4

At n=1 a closed rectangle is a closed interval [ak,bk] with ak≤bk and its volume is the length bk−ak, so the covers admitted in λcl(A) are exactly the covers admitted in the published definition of measure zero.

1.2F2F3

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 ε.

2.1step 1.1step 1.2L1∎

Hence A has measure zero in the published sense if and only if for every real ε>0 some admissible cover has total length at most ε, which says exactly that the infimum λcl(A) is 0; and λcl(A)=λ1∗(A).

Depends on

Used by

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