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.
Assuming countable choice, every measure space has a unique complete extension to its completion
Statement
Assume the Axiom of Countable Choice. Let be a measure space, and let be its completion construction. Then is a complete measure on extending . It is the unique complete measure on that extends .
Facts & Assumptions
Given: A measure space and the Axiom of Countable Choice.
The completion domain is a sigma-algebra containing (Assuming countable choice, the completion domain is a sigma-algebra).
The value is independent of the measurable core in a completed representation (The completed measure is independent of the representing measurable set).
Countable unions of measurable null sets are null, and completeness makes all their subsets measurable and null (Null sets are closed under countable unions and, in a complete space, under arbitrary subsets).
A measure vanishes at the empty set and is countably additive on disjoint measurable sequences (Measures on sigma-algebras).
Countable choice selects witnesses from each nonempty natural-number-indexed family (The Axiom of Countable Choice ()).
Every member of the completion domain has a representation with measurable and contained in a measurable null set, and the proposed completed value is (The completion domain and proposed completed set function of a measure space).
Proof
By [L1] and [L2], is a function on the sigma-algebra , and for by the representation ; in particular .
Let be disjoint in . By [L6] each family of completed representations is nonempty, so [L5] chooses with measurable and contained in a measurable null set . Then the are disjoint, with , and is null by [L3].
If and , choose a representation from [L6] with null. Then is measurable and null, and every is represented by the empty measurable core plus the sub-null set .
Let be any complete measure on extending . For a representation from [L6], with and , one has and completeness gives . Replacing by makes the union disjoint without changing , so finite additivity gives .
Countable additivity of applied to the measurable cores in step 1.2 gives ; with step 1.1, this proves that is a measure.
Step 1.3 shows that every subset of every -null set belongs to and has value , so the completed measure space is complete.
Steps 2.1, 2.2 and 1.4 prove respectively that is an extending measure, is complete, and is the unique complete extension on .
Depends on
- The completion domain and proposed completed set function of a measure space
- Assuming countable choice, the completion domain is a sigma-algebra
- The completed measure is independent of the representing measurable set
- Null sets are closed under countable unions and, in a complete space, under arbitrary subsets
- Measures on sigma-algebras
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Cited to discharge well-definedness by The completion domain and proposed completed set function of a measure space.
Dependency tree · two levels
19 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
- G. Folland, Real Analysis, 2nd ed., Theorem 1.9 (standard reference, not scraped)
- T. Tao, An Introduction to Measure Theory, Exercise 1.4.26 (standard reference, not scraped)