Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)judge 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.

Lebesgue outer measure on Rn

Definition

Fix n1. Lebesgue outer measure λn on Rn is the outer set function induced by the premeasure μ0 of Elementary volume is a sigma-finite premeasure on the algebra of elementary sets on the algebra En of elementary sets (Elementary sets: the finite unions of half-open boxes in Rn), in the sense of The outer set function induced by a premeasure:

λn(E)  :=  inf{ k=0μ0(Ak) : AkEn for every kN and EkNAk }

for ERn, the series being the nonnegative extended sum of Series in the nonnegative extended real line. The family of covering costs is nonempty, because RnEn and the sequence (Rn,,,) covers every E, so the infimum is a well-determined element of [0,+]. On the real line the subscript is dropped and λ:=λ1.

The values λn(E) are defined for every subset of Rn, with no measurability hypothesis. That the resulting set function is an outer measure, and that it agrees with μ0 on En, are proved in Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume; until then the name outer measure is not claimed, exactly as The outer set function induced by a premeasure stipulates.

Remarks

  • Why the covers are by elementary sets and not by boxes. Both give the same value, since an elementary set is a finite union of boxes and a countable family of finite lists reindexes to a countable family of boxes; taking elementary sets is what makes the definition an instance of the published construction, so that the Carathéodory theory applies with nothing reproved. The comparison with covers by closed, open and cubic boxes is Countable covers by closed boxes, by open boxes and by closed cubes all compute Lebesgue outer measure.

  • The definition itself spends no choice principle; it is an infimum of a nonempty subset of [0,+]. Countable choice enters only when the infimum is shown to be countably subadditive, and that is recorded where it happens.

Depends on

Used by

Dependency tree · two levels

22 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