Alphabeta Math
PropositionStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

Lebesgue measure is sigma-finite, and every metrically bounded subset of Rn has finite outer measure

Statement

Let n1 and assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Then:

  1. λn is sigma-finite (Finite, sigma-finite, and semifinite measures): the cubes (k,k]n are Lebesgue measurable with λn((k,k]n)=(2k)n<+, they increase with k, and their union over kN is Rn.
  2. Every bounded subset ERn (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space) has λn(E)<+; a bounded Lebesgue measurable set therefore has finite measure, and every compact subset of Rn is Lebesgue measurable of finite measure.

Facts & Assumptions

Given: A natural number n1, the Axiom of Countable Choice, and Lebesgue measure λn on L(Rn).

[L1]

Assuming countable choice, L(Rn) is a sigma-algebra, λn is a complete measure on it, and λn(B)=vol(B) for every half-open box B (Assuming countable choice, L(Rn) is a sigma-algebra containing every elementary set and λn is a complete measure extending elementary volume).

[L2]

Every set R with RRR is Lebesgue measurable with λn(R)=i<n(biai) (A box in Rn with parameters aibi is Lebesgue measurable of measure i<n(biai), whichever of its faces are included).

[L3]

Assuming countable choice, λn is an outer measure on Rn, hence monotone (Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume, Outer measures).

[L4]

Assuming countable choice, every Borel subset of Rn is Lebesgue measurable (Assuming countable choice, every Borel subset of Rn is Lebesgue measurable).

[L5]

For a nonempty box vol(B):=i<n(biai) when every ai and every bi is real, and (u,v]n:=B(u,v) (Half-open boxes in Rn and their volume, Integer powers am).

[F1]

μ is sigma-finite if there is a sequence (En)nN in A such that X=nEn and μ(En)<+ for every n (Finite, sigma-finite, and semifinite measures).

[F2]

A is bounded if A= or there are x0X and a real r>0 with AB(x0,r), where B(x0,r):={y:d(x0,y)<r} (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Open ball, closed ball and sphere in a metric space).

[F5]

If A,BA and AB, then μ(A)μ(B) (Measures are monotone).

[F6]

Every complete ordered field F is Archimedean: for every xF there is a natural number n1 with x<n1F (Every complete ordered field is Archimedean).

Proof

technique · direct
1.1

Each cube (k,k]n is a half-open box, hence Lebesgue measurable with λn((k,k]n)=i<n(k(k))=(2k)n, a real number; the cubes increase with k; and every xRn lies in one of them, because the Archimedean property gives a natural k1 above each of the finitely many reals xi, so their union is Rn and λn is sigma-finite.

L1L2L5F1F6
1.2

Let E be bounded and nonempty, say EB(x0,r) with r a positive real; every yE satisfies yi(x0)id2(x0,y)<r in each coordinate, so E is contained in the half-open box with parameter pairs ((x0)ir, (x0)i+r], whose volume is (2r)n; monotonicity of the outer measure therefore gives λn(E)(2r)n<+, and the empty set has outer measure 0.

L1L3L5F2F3
2.1

A bounded Lebesgue measurable set has λn(E)=λn(E)<+ by step 1.2; and a compact KRn is closed, hence Borel and Lebesgue measurable, and bounded, hence of finite measure.

step 1.2L4F4F5
3.1

Step 1.1 is claim 1 and steps 1.2 and 2.1 are claim 2.

step 1.1step 1.2step 2.1

Depends on

Used by

Dependency tree · two levels

116 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