Baire sequence space is homeomorphic to the irrational real numbers

Given: The objects, hypotheses, and choice principles stated above.

The Baire sequence space is $\mathcal{N}:={\mathbb{N}}^{\mathbb{N}}$, the set of functions from $\mathbb{N}$ to itself (def-the-set-of-functions-from-one-set-to-another), with the product topology obtained by giving each copy of $\mathbb{N}$ the discrete topology (def-product-topology, def-standard-topologies). For a finite sequence $s=(s_0,\dots ,s_{k-1})$, its cylinder is $N_s:=\{x\in \mathcal{N}:x_i=s_i\text{ for }i<k\}$. The empty sequence has cylinder $\mathcal{N}$, and these cylinders form a basis. (Baire sequence space ${\mathbb{N}}^{\mathbb{N}}$ and its cylinder topology).

The continued-fraction coding determined by def-simple-continued-fraction-coding gives a bijection from the sequences $(a_0,a_1,\dots )$ with $a_0\in \mathbb{Z}$ and $a_n\ge 1$ for $n\ge 1$ onto $\mathbb{R}\setminus \mathbb{Q}$. Both the coding map and its inverse are continuous for the cylinder and subspace topologies. (Infinite simple continued fractions parametrise the irrational real numbers).