LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-09-24 (gpt-6-sol)

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 countable union of compact content-zero subsets of the line is null in ZF

Statement

In ZF, let $(K_{n})_{n \in N}$ be a sequence of compact subsets of $R$ , each of content zero in the sense of Measure zero (a countable cover by intervals of total length below every $ε$ ) and content zero (a finite such cover). Then $⋃_{n \in N} K_{n}$ has measure zero. No countable choice is required.

Facts & Assumptions

Given: A sequence $(K_{n})$ as in the Statement and a real $ε > 0$ .

[L1]

Content zero gives, for each positive budget, a finite closed-interval cover with total length at most that budget; nullity asks for one countable closed-interval cover whose partial length sums are at most $ε$ (Measure zero (a countable cover by intervals of total length below every $ε$ ) and content zero (a finite such cover)).

[L2]

Between two distinct reals lies a rational (ℚ is dense in every Archimedean ordered field), so finitely many closed real intervals can be enlarged to open intervals with rational endpoints at arbitrarily small extra total length.

[L3]

The explicit bijection $J : N^{2} \to N$ from $N \times N \approx N$ codes finite sequences recursively by $C (()) = 0$ and $C ((a_{0}, \dots, a_{k - 1})) = 1 + J (a_{0}, C ((a_{1}, \dots, a_{k - 1})))$ . This is injective: code $0$ means empty, and for positive valid codes $J^{- 1}$ uniquely recovers the first entry and tail code, and that tail code is smaller than the whole code because $J (a, b) \geq b$ . Integers have the explicit coding $z \mapsto 2 z$ for $z \geq 0$ and $z \mapsto - 2 z - 1$ for $z < 0$ ; rationals are integer fractions (The rationals as equivalence classes of pairs of integers), so fractions $m / k$ with $k > 0$ admit natural codes. Decoding invalid codes as zero gives an explicit surjection $r : N \to Q$ . Together these codes enumerate every finite list of pairs of rational endpoints.

[L4]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

[L5]

There is an explicit bijection $J : N \times N \to N$ ( $N \times N \approx N$ ). For $b_{n} = ε 2^{- n - 1}$ , every finite partial sum $\sum_{n \leq N} b_{n}$ is at most $ε$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges, Laws of finite sums and finite products).

Proof

technique · direct

1.1

Fix $n$ and put $b_{n} = ε 2^{- n - 1} > 0$ . By [L1], $K_{n}$ has a finite closed-interval cover with total length at most $b_{n} / 2$ . Enlarge each of its finitely many intervals using [L2], spending in total less than $b_{n} / 2$ in extra length. The resulting finite family of rational open intervals covers $K_{n}$ and has total length less than $b_{n}$ . Closing those rational intervals preserves their lengths and still covers $K_{n}$ .

L1L2L5choose

1.2

By [L3], let $C_{c}$ be the finite list of rational closed intervals decoded from $c \in N$ when it is a valid list code, and let invalid codes decode to the one-term list $[0, 0]$ . The set $S_{n} = {c \in N : K_{n} \subseteq ⋃ C_{c} and the total length of C_{c} is < b_{n}}$ is nonempty by step 1.1. Define $c_{n} : = \min S_{n}$ by [L4]. The formula for $S_{n}$ and least-number selection define the entire sequence $(c_{n})$ in ZF; no independent choice of covers is made.

L3L4step 1.1construct

2.1

Write $C_{c_{n}} = ([a_{n, 0}, d_{n, 0}], \dots, [a_{n, l_{n} - 1}, d_{n, l_{n} - 1}])$ . Extend each finite list to all $j \in N$ by $[a_{n, j}, d_{n, j}] = [0, 0]$ for $j \geq l_{n}$ . For $k = J (n, j)$ , set $[A_{k}, D_{k}] = [a_{n, j}, d_{n, j}]$ . Because $J$ is a bijection, this defines a sequence of closed intervals covering every $K_{n}$ , hence their union.

L3L5step 1.2construct

3.1

Fix any finite partial list $k < t$ . Its inverse $J$ -coordinates lie in some finite rectangle $n, j \leq N$ . All lengths are nonnegative, so its total length is at most the sum of the full finite list lengths for $n \leq N$ . Each such length is $< b_{n}$ by step 1.2, whence the partial total is at most $\sum_{n \leq N} b_{n} \leq ε$ by [L5].

L5step 1.2step 2.1algebra

4.1

Steps 2.1 and 3.1 meet the covering and partial-sum conditions of [L1] for the given $ε$ . As $ε > 0$ was arbitrary, $⋃_{n} K_{n}$ is null. The only selections were finite choices in step 1.1 and least natural-number codes in step 1.2, both available in ZF.

L1step 2.1step 3.1∎

Source notes

Hunter, §11.8, pp. 238–239, states the Lebesgue criterion and uses geometric $ε / 2^{k}$ cover budgets. It states the criterion without proof and does not give the least-code construction above. The choice-free coding argument is proved here from the listed local suppliers.

Depends on

Used by

Dependency tree · two levels

61 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, An Introduction to Real Analysis, Chapter 11 (standard reference, not scraped)