Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)
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.

For a compact subset of R\mathbb{R}, measure zero and content zero coincide

Statement

Let KRK \subseteq \mathbb{R} be compact (Open cover, subcover, compact subset of R\mathbb{R} (every open cover has a finite subcover), and sequentially compact subset), equivalently closed and bounded (A subset of R\mathbb{R} is compact if and only if it is closed and bounded). Then

K has measure zeroK has content zeroK \text{ has measure zero} \quad \Longleftrightarrow \quad K \text{ has content zero}

(Measure zero (a countable cover by intervals of total length below every ε\varepsilon) and content zero (a finite such cover)).

The implication from content zero to measure zero is A set of content zero has measure zero and needs no hypothesis on KK. The other direction is the one that uses compactness, and it uses it exactly as A sequence of intervals covering [a,b][a,b] has total length at least bab - a, so no interval of positive length has measure zero does: a countable cover is enlarged to an open cover at an arbitrarily small cost in total length, and compactness reduces the open cover to a finite one.

Facts & Assumptions

Given: A compact set KRK \subseteq \mathbb{R} and a real ε>0\varepsilon > 0. Throughout, θ:=21\theta := 2^{-1}.

[L1]

AA is null when for every real η>0\eta > 0 there are sequences (ak)(a_k), (bk)(b_k) with akbka_k \le b_k, Ak[ak,bk]A \subseteq \bigcup_k[a_k,b_k] and k<i(bkak)η\sum_{k<i}(b_k - a_k) \le \eta for every ii; AA has content zero when the same holds with a finite list (Measure zero (a countable cover by intervals of total length below every ε\varepsilon) and content zero (a finite such cover)).

[L2]

A set of content zero is null (A set of content zero has measure zero).

[L3]

[c,d][c,d] has length dc0d - c \ge 0 for cdc \le d; (c,d)(c,d) is the open interval with the same endpoints and is contained in [c,d][c,d] (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length).

[L5]

KK is compact: from every family of open sets whose union contains KK, either K=K = \varnothing and the empty subfamily covers it, or there are mNm \in \mathbb{N} and members U0,,UmU_0, \dots, U_m of the family whose union contains KK; compactness is equivalent to being closed and bounded (Open cover, subcover, compact subset of R\mathbb{R} (every open cover has a finite subcover), and sequentially compact subset, A subset of R\mathbb{R} is compact if and only if it is closed and bounded).

[L6]

Powers and the geometric series: θ0=1\theta^0 = 1, θk+1=θkθ\theta^{k+1} = \theta^k\theta, θk>0\theta^k > 0, and k=0θk=2\sum_{k=0}^{\infty}\theta^k = 2 for θ=21\theta = 2^{-1}; a series of nonnegative terms has all its partial sums at most its sum (Integer powers ama^m, For r<1|r| < 1, k0rk=1/(1r)\sum_{k \ge 0} r^k = 1/(1-r), and for r1|r| \ge 1 the series diverges, Series, partial sums, convergence and the sum, divergence, and the tail series, A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum).

[L7]

Finite sums: additivity, scaling, splitting and monotonicity in the terms (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L8]

Every finite list of naturals has an upper bound in N\mathbb{N}, by induction on its length and the totality of the order of N\mathbb{N} (The principle of mathematical induction, Trichotomy of the order on N\mathbb{N}, Order on the natural numbers).

[L9]

Ordered-field arithmetic: 0<10 < 1, so 2>02 > 0, 4>04 > 0, 8>08 > 0 and t81>0t \cdot 8^{-1} > 0 for t>0t > 0; adding a constant and multiplying by a positive preserve an inequality (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property)). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.

Proof

technique · direct
1.1

One direction is immediate: if KK has content zero then KK is null by [L2], with no hypothesis on KK used. It remains to prove the converse for compact KK.

L2suffices: only the forward direction remains
1.2

If K=K = \varnothing, then for every real ε>0\varepsilon > 0 the single interval [0,0][0,0] covers KK and has total length 0ε0 \le \varepsilon, so KK has content zero by [L1]. Hence suppose KK \ne \varnothing for the rest of the proof.

L1cases
2.1

Assume KK is null and let the real ε>0\varepsilon > 0 be given. By [L1] applied with η:=ε21>0\eta := \varepsilon \cdot 2^{-1} > 0 fix sequences (ak)(a_k), (bk)(b_k) with akbka_k \le b_k, Kk[ak,bk]K \subseteq \bigcup_k [a_k,b_k] and k<i(bkak)ε21\sum_{k<i}(b_k - a_k) \le \varepsilon \cdot 2^{-1} for every iNi \in \mathbb{N}.

step 1.1givenL1L9choose
3.1

Put δk:=ε81θk\delta_k := \varepsilon \cdot 8^{-1} \cdot \theta^{k}, a positive real by [L6] and [L9], and Jk:=(akδk, bk+δk)J_k := (a_k - \delta_k,\ b_k + \delta_k), an open set by [L4] containing [ak,bk][a_k,b_k] by [L3] and [L9]. Hence {Jk:kN}\{\, J_k : k \in \mathbb{N} \,\} is a family of open sets whose union contains KK, and the closed interval [akδk, bk+δk][a_k - \delta_k,\ b_k + \delta_k] has length (bkak)+2δk=(bkak)+ε41θk(b_k - a_k) + 2\delta_k = (b_k - a_k) + \varepsilon \cdot 4^{-1} \cdot \theta^{k} by [L3] and [L9].

step 2.1L3L4L6L9
4.1

By [L5] there are mNm \in \mathbb{N} and members Jk0,,JkmJ_{k_0}, \dots, J_{k_m} of that family covering KK, and by [L8] there is NNN \in \mathbb{N} with ktNk_t \le N for every tmt \le m; then KkNJkkN[akδk, bk+δk]K \subseteq \bigcup_{k \le N} J_k \subseteq \bigcup_{k \le N}[a_k - \delta_k,\ b_k + \delta_k] by [L3].

step 1.2step 3.1L3L5L8choose
5.1

The total length of that finite list is kN((bkak)+ε41θk)=k<N+1(bkak)+ε41k<N+1θkε21+ε412=ε\sum_{k \le N}\big((b_k - a_k) + \varepsilon \cdot 4^{-1}\theta^{k}\big) = \sum_{k<N+1}(b_k - a_k) + \varepsilon \cdot 4^{-1}\sum_{k<N+1}\theta^{k} \le \varepsilon \cdot 2^{-1} + \varepsilon \cdot 4^{-1} \cdot 2 = \varepsilon, by [L7], step 2.1, [L6] and [L9].

step 2.1step 3.1step 4.1L6L7L9
6.1

So for every real ε>0\varepsilon > 0 the finite list of step 4.1 covers KK with total length at most ε\varepsilon, which by [L1] is exactly the statement that KK has content zero; together with step 1.1 the two notions coincide on compact sets.

step 1.1step 1.2step 4.1step 5.1L1

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 116 results over 29 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources