TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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, a generated sigma-algebra is obtained in omega-one stages of complements and countable unions

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ . Let $X$ be a set and $E \subseteq P (X)$ . Define families $(E_{α})_{α < ω_{1}}$ by

$E_{0} : = E \cup {\emptyset},$

$E_{α + 1} : = {X ∖ A : A \in E_{α}} \cup {⋃_{n \in N} A_{n} : (A_{n})_{n \in N} is a sequence in E_{α}},$

and $E_{λ} : = ⋃_{α < λ} E_{α}$ at every nonzero limit ordinal $λ < ω_{1}$ . Then

$σ_{X} (E) = ⋃_{α < ω_{1}} E_{α} .$

Facts & Assumptions

Given: The Axiom of Countable Choice, a set $X$ , and a family $E \subseteq P (X)$ .

[L1]

Transfinite recursion on a well-order produces a unique function whose value at each stage is prescribed from all earlier values (Transfinite recursion).

[L2]

Under ${A C}_{ω}$ , every at most countable subset of $ω_{1}$ is bounded below $ω_{1}$ (Assuming countable choice: every at most countable subset of $ω_{1}$ is bounded below $ω_{1}$ , so no at most countable subset of $ω_{1}$ is cofinal in it, and a supremum of at most countably many at most countable ordinals is at most countable).

[L3]

The Axiom of Countable Choice supplies a choice function for every family of nonempty sets indexed by $N$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L4]

The family $σ_{X} (E)$ exists and is the smallest sigma-algebra on $X$ containing $E$ (Nonempty intersections of sigma-algebras are sigma-algebras, so the generated sigma-algebra exists and is minimal).

Proof

technique · direct

1.1

The displayed successor and limit prescriptions define a class function of the earlier stages, so [L1] produces the unique family $(E_{α})_{α < ω_{1}}$ . Each stage is contained in the next because $A$ is the union of the constant sequence with value $A$ .

L1construct

2.1

Transfinite induction gives $E_{α} \subseteq σ_{X} (E)$ for every $α < ω_{1}$ : at the base, the generated sigma-algebra contains $E$ and $\emptyset$ ; complements and countable unions stay in the sigma-algebra at a successor stage; and a limit stage is a union of earlier subfamilies.

step 1.1L4

2.2

Put $S : = ⋃_{α < ω_{1}} E_{α}$ . It contains $E$ and $\emptyset$ and is closed under complements. Given $(A_{n})$ in $S$ , [L3] may choose stages $α_{n}$ with $A_{n} \in E_{α_{n}}$ ; [L2] bounds the set of chosen stages by some $β < ω_{1}$ . Monotonicity from step 1.1 puts every $A_{n}$ in $E_{β}$ , so $⋃_{n} A_{n} \in E_{β + 1} \subseteq S$ . Thus $S$ is a sigma-algebra.

step 1.1L2L3

3.1

Minimality in [L4] gives $σ_{X} (E) \subseteq S$ , while step 2.1 gives the reverse inclusion. Hence the two families are equal.

step 2.1step 2.2L4∎

Depends on

Used by

Assuming the Axiom of Choice, an infinite family E generates at most |E|ᵃleph-zero sets Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 54 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

T. Tao, An Introduction to Measure Theory, Exercise 1.4.15 (standard reference, not scraped)
D. H. Fremlin, Measure Theory, Chapter 56, result 567E(b) (standard reference, not scraped)