Under Dependent Choice, every nonempty Polish space is a continuous image of Baire sequence space

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).

A topological space is Polish when it is separable (def-separable-space) and completely metrizable: its topology is induced by some complete metric (lem-complete-remetrisation). No particular compatible complete metric or countable dense subset is part of the structure. (Polish spaces are separable completely metrizable spaces).

Let $X$ be a set and let $R\subseteq X\times X$ be a binary relation on $X$. Call $R$ entire on $X$ when $\text{for every }x\in X\text{ there is }y\in X\text{ with }xRy\mathrm{.}$ The Axiom of Dependent Choice, written $\mathrm{D}\mathrm{C}$, is the following statement. The statement is: for every nonempty set $X$, every relation $R$ entire on $X$, and every $a\in X$, there is a sequence $x:\mathbb{N}\to X$ with $x_0=a$ and $x_{n}R{x}_{n+1}$ for every $n\in \mathbb{N}$. (The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain).

Let $(X,d)$ be a metric space (def-metric-space). Call a sequence $(F_k{)}_{k\in \mathbb{N}}$ of subsets of $X$ a Cantor chain if every $F_k$ is nonempty, closed (def-metric-topology) and bounded, $F_{k+1}\subseteq F_k$ for every $k$, and $\mathrm{diam}(F_k)\to 0$ in $\mathbb{R}$ (def-metric-bounded-diameter, def-real-limit). Then: 1. If $(X,d)$ is complete (def-complete-metric-space), every Cantor chain in $X$ has an intersection ${\bigcap }_{k\in \mathbb{N}}{F}_k$ with exactly one element. 2. Conversely, if every Cantor chain in $X$ has nonempty intersection, then $(X,d)$ is complete. Boundedness of each $F_k$ is part of the definition of a Cantor chain because $\mathrm{diam}$ is defined for nonempty bounded sets only in this library (def-metric-bounded-diameter); it is not an extra hypothesis but the precondition for writing the diameter condition down. (In a complete metric space nested nonempty closed sets whose diameters tend to $0$ meet in exactly one point, and this property characterises completeness).

Let $(X,d)$ be a metric space (def-metric-space), let $x\in X$ and let $r\in \mathbb{R}$ with $r>0$ (def-real-order). Define $B(x,r):=\{y\in X:d(x,y)<r\},\bar{B}(x,r):=\{y\in X:d(x,y)\le r\},S(x,r):=\{y\in X:d(x,y)=r\}\mathrm{.}$ $B(x,r)$ is the open ball, $\bar{B}(x,r)$ the closed ball and $S(x,r)$ the sphere of centre $x$ and radius $r$. The radius is always a strictly positive real; a ball of radius $0$ or of negative radius is never written in this library. (Open ball, closed ball and sphere in a metric space).