Alphabeta MathHow 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.
A product of two at most countable sets is at most countable
Statement
If and are at most countable (Finite, countably infinite, countable, uncountable) then so is .
No choice principle is used: the two enumerations are given, and the enumeration of the product is written down from them.
Facts & Assumptions
Given: At most countable sets and , and the product .
Finite, countably infinite and at most countable; , so is finite (Finite, countably infinite, countable, uncountable, The natural numbers (von Neumann)).
A nonempty set is at most countable if and only if some surjection it exists (A nonempty set is at most countable iff it is a surjective image of ).
There is a bijection (, Equinumerous sets, and ).
A composition of surjections is a surjection (Injection, surjection, bijection).
Proof
If or then , which is finite and hence at most countable.
Assume instead and ; then [L2] provides surjections and .
Fix the bijection of [L3], in particular a surjection.
Define by . It is surjective: any has and for some , so .
Hence is a surjection by [L4], and is nonempty, so it is at most countable by [L2].
Both cases give the conclusion: is at most countable whenever and are.
Remarks
-
Iterating gives the same conclusion for for each fixed : is a product of two at most countable sets, and so on, so applications of the theorem settle the case . Stating this uniformly in , as a single theorem quantified over , needs finite sequences of sets and a recursive definition of the -fold product, which this library does not yet have; the iterated form above is the honest statement of what is proved.
-
The infinite product is a different matter and is not covered: is a product of countably many two-element sets and is uncountable, by the same diagonal argument as Cantor's theorem: . Countability is not preserved by infinite products of any kind.
-
Together with Every subset of an at most countable set is at most countable this gives the countability of every set that can be coded by finitely many naturals, which is how is countably infinite is proved.
Depends on
- $\mathbb{N} \times \mathbb{N} \approx \mathbb{N}$
- Finite, countably infinite, countable, uncountable
- A nonempty set is at most countable iff it is a surjective image of $\mathbb{N}$
- Equinumerous sets, $A \approx B$ and $A \preceq B$
- Injection, surjection, bijection
- The natural numbers $\mathbb{N}$ (von Neumann)
Used by
- c₀ is not isomorphic to a dual space Corollary
- Countable levels do not suffice for König’s lemma Counterexample
- Connection on a smooth vector bundle Definition
- The circle, rotations and the doubling map Definition
- Wiener measure on continuous path space Definition
- Assuming countable choice, a strictly increasing ω-sequence of countable ordinals has a countable supremum, which is a countable limit ordinal below ω₁; the instance supₙ ω·(n+1) = ω² needs no choice Example
- Euclidean borel spaces are standard borel Example
- ℝ as a vector space over ℚ has a basis, and every such basis is infinite; the existence proof exhibits none Example
- ℝ with the half-open intervals [a,b) as a basis is not compact and, assuming the Axiom of Countable Choice, is Lindel"of, while its square is not Lindel"of, the antidiagonal being an uncountable closed discrete subspace Example
- The one-point compactification of the discrete real line is compact and Lindelöf but is neither first countable nor separable Example
- The Sorgenfrey plane: the product of two half-open-interval lines has the rectangles [a,b) × [c,d) as a basis and ℚ × ℚ as a countable dense subset Example
- Under choice, the Niemytzki plane is Tychonoff and locally metrizable but not normal, paracompact, or metrizable Example
- ω + ω is at most countable although it is not order isomorphic to ω: order type and cardinality are different invariants Example
- Refuted: separability is hereditary False statement
- A countable dense family of continuous functions on a compact metric space Lemma
- A countable generator of a sigma-algebra yields a countable algebra of sets Lemma
- Borel sigma-algebra of continuous path space is generated by coordinates Lemma
- Borel subspaces admit polish presentations Lemma
- Countable compactness closes in the bidual Lemma
- Eberlein–Šmulian separable reduction Lemma
- Every compact subset of a Bernstein set is countable Lemma
- Every finite power of an at most countable set is at most countable Lemma
- Rational bounds at countable limit levels Lemma
- Regular conditional kernels factor through a standard borel conditioning variable Lemma
- Simultaneous rational conditional distribution function versions Lemma
- The lower-limit plane has a countable dense set and a closed discrete antidiagonal of size |ℝ| Lemma
- Under countable choice, continuous path space is Polish Lemma
- Sequence ell-one versus nonatomic L-one for the RNP Remark
- A special Aronszajn tree exists Theorem
- Almost every point is a Lebesgue point of a locally integrable function Theorem
- Assuming countable choice, a countable product of first countable spaces is first countable Theorem
- Assuming countable choice, a countable product of second countable spaces is second countable Theorem
- Assuming countable choice, countable covering costs define an outer measure Theorem
- Assuming countable choice, every measure is the sum of its semifinite part and a zero-infinity-valued measure Theorem
- Cramer wold device Theorem
- Every nonempty perfect subset of ℝ has the cardinality of the continuum Theorem
- Every open subset of ℝⁿ is the union of a countable pairwise disjoint family of dyadic cubes Theorem
- Finite specialization of an Aronszajn tree is ccc Theorem
- Poles of a meromorphic function form a closed discrete set and are at most countable Theorem
- ℚ is countably infinite Theorem
…and 3 more results.
Dependency tree · two levels
40 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
- J. K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)
- J. Lebl, Basic Analysis: Introduction to Real Analysis, basic set theory (standard reference, not scraped)
- Countable set (Wikipedia) (standard reference, not scraped)
- T. Tao, Analysis I, 3rd ed., §8.1 (standard reference, not scraped)