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 . If is an infinite sigma-algebra on , then there is an injection . Consequently is uncountable (Finite, countably infinite, countable, uncountable).
Facts & Assumptions
Given: The Axiom of Countable Choice and an infinite sigma-algebra on .
Countable choice selects one member from every sequence of nonempty sets (The Axiom of Countable Choice ()).
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).
A sigma-algebra is closed under countable unions (Sigma-algebras).
The power set of a set is strictly larger than the set itself (Cantor's theorem: ), with domination expressed by injections (Equinumerous sets, and ).
An at most countable set is finite or equinumerous with , and in either case it injects into (Finite, countably infinite, countable, uncountable).
Under , a countable union of at most countable sets is at most countable (Countable unions of at most countable sets, assuming ).
Proof
For each , let be the nonempty set of injections . By [L1] choose . By [L6], the union of the finite ranges 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 .
By [L2], fix pairwise disjoint nonempty . For , define , which lies in by [L3].
If , the least index in belongs to exactly one of them, and its nonempty is contained in exactly one of by disjointness. Thus is injective. If were at most countable, [L5] would give an injection ; the map that sends to and every natural number outside to would then be a surjection , contrary to [L4]. Hence is uncountable.
Depends on
- A sigma-algebra with a listed infinite subfamily contains a disjoint sequence of nonempty members
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Countable unions of at most countable sets, assuming $\mathrm{AC}_\omega$
- Cantor's theorem: $A \prec \mathcal{P}(A)$
- Equinumerous sets, $A \approx B$ and $A \preceq B$
- Sigma-algebras
- Finite, countably infinite, countable, uncountable
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
- R. F. Bass, Real Analysis for Graduate Students, version 5.0, Exercise 2.6 (standard reference, not scraped)