Theorem·T55

n-tuples from a countable set are countable

Fixed-length tuples from a countable set are countable, by peeling off the last entry and inducting on the length.

For a countable set and :

In words

For a countable set X and any natural number n: the set of length-n tuples from X is countable.

Never needed: F10 · F13 · A03 · A04 · A05 · A07 · A09 (computed from the citation graph, not asserted).

Proof

1
By induction on .
2
Base, . (D085), a single-point set, hence finite and so countable.
3
Step. Assume is countable (the induction hypothesis, "IH"); show is countable. Define by (well-defined: and , as ). Suppose : by L01, and . Since both have domain , agree on all of (from ) and agree at : (Extensionality). So is an injection.
4
By the IH and T54, is countable; since injects into it, composing with a witnessing injection (L02) gives , i.e. countable.
5
T05 concludes: is countable for every .

∎

Feeds directly into countability of all finite sequences: (D074, D085), an -indexed union of the countable sets just shown countable here.

Propose an edit1 published revision