Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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, every infinite sigma-algebra contains a copy of the power set of the natural numbers

Statement

Assume ACω. If A is an infinite sigma-algebra on X, then there is an injection P(N)A. Consequently A is uncountable (Finite, countably infinite, countable, uncountable).

Facts & Assumptions

Given: The Axiom of Countable Choice and an infinite sigma-algebra A on X.

[L1]

Countable choice selects one member from every sequence of nonempty sets (The Axiom of Countable Choice (ACω)).

[L2]

A sigma-algebra with an injective sequence of members contains a sequence of pairwise disjoint nonempty members (A sigma-algebra with a listed infinite subfamily contains a disjoint sequence of nonempty members).

[L3]

A sigma-algebra is closed under countable unions (Sigma-algebras).

[L4]

The power set of a set is strictly larger than the set itself (Cantor's theorem: AP(A)), with domination expressed by injections (Equinumerous sets, AB and AB).

[L5]

An at most countable set is finite or equinumerous with N, and in either case it injects into N (Finite, countably infinite, countable, uncountable).

[L6]

Under ACω, a countable union of at most countable sets is at most countable (Countable unions of at most countable sets, assuming ACω).

Proof

technique · constructive
1.1

For each m1, let Im be the nonempty set of injections mA. By [L1] choose fmIm. By [L6], the union of the finite ranges fm[m] is at most countable. It is infinite because it has subsets of every finite size, so [L5] makes it countably infinite; a bijective listing is therefore an injective sequence in A.

L1L5L6construct
2.1

By [L2], fix pairwise disjoint nonempty DnA. For SN, define Φ(S):=nSDn, which lies in A by [L3].

step 1.1L2L3construct
3.1

If ST, the least index in ST belongs to exactly one of them, and its nonempty Dn is contained in exactly one of Φ(S),Φ(T) by disjointness. Thus Φ is injective. If A were at most countable, [L5] would give an injection j:AN; the map that sends j(Φ(S)) to S and every natural number outside j[Φ[P(N)]] to would then be a surjection NP(N), contrary to [L4]. Hence A is uncountable.

step 2.1L4L5discharge-construct

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 53 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