Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27
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 the Lebesgue-Stieltjes measure of the identity function

Statement

Assume the Axiom of Countable Choice. Let id⁡R(x):=x. The Lebesgue-Stieltjes measure attached to id⁡R agrees with Lebesgue measure λ from Lebesgue measurable sets, the family L(Rn), and the restricted set function λn on every Borel subset of R.

Facts & Assumptions

Given: Countable choice and the identity function id⁡R:R→R.

[L1]

Assuming countable choice, every nondecreasing right-continuous function on R defines a Borel measure through the Lebesgue-Stieltjes construction. (Assuming countable choice, a nondecreasing right-continuous function defines a Borel measure on R)

[L2]

For every half-open interval (a,b]⊆R, Lebesgue measure satisfies λ((a,b])=b−a. (A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included)

[L3]

A Borel measure on R finite on compact sets is uniquely determined by its values on half-open intervals. (The interval data on (a,b] determines the Borel measure uniquely)

Proof

technique · direct
1.1L1

The identity function is nondecreasing and right-continuous, so [L1] gives a Borel measure μid⁡ with

μid⁡((a,b])=id⁡R(b)−id⁡R(a)=b−a.

[L1]

1.2L2

By [L2], Lebesgue measure has the same half-open interval values: λ((a,b])=b−a for every a<b.

2.1step 1.1step 1.2L3

The measures μid⁡ and λ are both Borel and finite on compact sets, and by steps 1.1 and 1.2 they agree on every half-open interval.

Therefore [L3] gives μid⁡=λ. [step 1.1, step 1.2, L3] ∎

Depends on

Used by

Dependency tree · two levels

25 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