LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21

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, the completion domain is a sigma-algebra

Statement

Assume the Axiom of Countable Choice. For every measure space $(X, A, μ)$ , the completion domain $\overline{A}$ of The completion domain and proposed completed set function of a measure space is a sigma-algebra on $X$ containing $A$ .

Facts & Assumptions

Given: A measure space $(X, A, μ)$ and the Axiom of Countable Choice.

[L1]

The completion domain consists of the sets $A \cup N$ with $A, Z \in A$ , $N \subseteq Z$ , and $μ (Z) = 0$ (The completion domain and proposed completed set function of a measure space).

[L2]

A sigma-algebra contains the empty set, is closed under relative complements, and is closed under countable unions (Sigma-algebras).

[L3]

A countable union of measurable null sets is measurable and null (Null sets are closed under countable unions and, in a complete space, under arbitrary subsets).

[L4]

Countable choice selects one member from every nonempty natural-number-indexed family (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

1.1givenL1L2

Every $A \in A$ belongs to $\overline{A}$ by taking $N = Z = \emptyset$ ; in particular $\emptyset, X \in \overline{A}$ .

1.2givenL1L2

If $E = A \cup N$ with $N \subseteq Z$ , $μ (Z) = 0$ , replace $N$ by $N ∖ A$ without changing $E$ . Then $A$ and $N$ are disjoint, and $E^{c} = (A^{c} ∖ Z) \cup ((A^{c} \cap Z) ∖ N)$ , whose first part is measurable and whose second lies in the measurable null set $Z$ ; hence $E^{c} \in \overline{A}$ .

1.3givenL1L4choose

Let $(E_{k})$ be a sequence in $\overline{A}$ . For each $k$ , the family of triples $(A, N, Z)$ witnessing [L1] is nonempty, so [L4] selects $E_{k} = A_{k} \cup N_{k}$ with $N_{k} \subseteq Z_{k}$ and $μ (Z_{k}) = 0$ .

2.1step 1.3L2L3

Put $A = ⋃_{k} A_{k}$ and $Z = ⋃_{k} Z_{k}$ . Then $A, Z \in A$ , $μ (Z) = 0$ by [L3], and $(⋃_{k} E_{k}) ∖ A \subseteq Z$ , so $⋃_{k} E_{k} \in \overline{A}$ .

3.1step 1.1step 1.2step 2.1L2∎

Step 1.1 gives the empty set and containment of $A$ , step 1.2 gives complements, and step 2.1 gives countable unions; therefore $\overline{A}$ is a sigma-algebra.

Depends on

Used by

Assuming countable choice, every measure space has a unique complete extension to its completion Theorem

Cited to discharge well-definedness by The completion domain and proposed completed set function of a measure space.

Dependency tree · two levels

14 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)