TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (openai/gpt-5.4)verified 2026-07-26 (claude-opus-5)

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.

A product of two at most countable sets is at most countable

Statement

If $A$ and $B$ are at most countable (Finite, countably infinite, countable, uncountable) then so is $A \times B$ .

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 $A$ and $B$ , and the product $A \times B = \{\, (a,b) : a \in A,\ b \in B \,\}$ .

[L1]

Finite, countably infinite and at most countable; $\varnothing \approx 0$ , so $\varnothing$ is finite (Finite, countably infinite, countable, uncountable, The natural numbers $\mathbb{N}$ (von Neumann)).

[L2]

A nonempty set is at most countable if and only if some surjection $\mathbb{N} \to$ it exists (A nonempty set is at most countable iff it is a surjective image of $\mathbb{N}$ ).

[L3]

There is a bijection $\beta : \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ ( $\mathbb{N} \times \mathbb{N} \approx \mathbb{N}$ , Equinumerous sets, $A \approx B$ and $A \preceq B$ ).

[L4]

A composition of surjections is a surjection (Injection, surjection, bijection).

Proof

technique · direct

1.1

If $A = \varnothing$ or $B = \varnothing$ then $A \times B = \varnothing$ , which is finite and hence at most countable.

givenL1

1.2

Assume instead $A \ne \varnothing$ and $B \ne \varnothing$ ; then [L2] provides surjections $f : \mathbb{N} \to A$ and $g : \mathbb{N} \to B$ .

givenL2

1.3

Fix the bijection $\beta : \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ of [L3], in particular a surjection.

2.1

Define $t : \mathbb{N} \times \mathbb{N} \to A \times B$ by $t(m,n) = (f(m), g(n))$ . It is surjective: any $(a,b) \in A \times B$ has $a = f(m)$ and $b = g(n)$ for some $m, n$ , so $(a,b) = t(m,n)$ .

step 1.2

3.1

Hence $t \circ \beta : \mathbb{N} \to A \times B$ is a surjection by [L4], and $A \times B$ is nonempty, so it is at most countable by [L2].

step 1.3step 2.1L2L4

4.1

Both cases give the conclusion: $A \times B$ is at most countable whenever $A$ and $B$ are.

step 1.1step 3.1L1∎

Remarks

Iterating gives the same conclusion for $A_1 \times A_2 \times \dots \times A_k$ for each fixed $k$ : $(A_1 \times A_2) \times A_3$ is a product of two at most countable sets, and so on, so $k - 1$ applications of the theorem settle the case $k$ . Stating this uniformly in $k$ , as a single theorem quantified over $k$ , needs finite sequences of sets and a recursive definition of the $k$ -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: $\{0,1\}^{\mathbb{N}}$ is a product of countably many two-element sets and is uncountable, by the same diagonal argument as Cantor's theorem: $A \prec \mathcal{P}(A)$ . 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 $\mathbb{Q}$ is countably infinite is proved.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 56 results over 23 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

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)