Closed subspaces, products, and Baire parametrization

For two nonempty Polish spaces choose compatible complete metrics $d,e$ and countable dense sets $D,E$ by F1. On the product put $q((x,y),(x^{\mathrm{\prime }},y^{\mathrm{\prime }}))=d(x,x^{\mathrm{\prime }})+e(y,y^{\mathrm{\prime }})$. Each product neighbourhood contains a q-ball, and each q-ball contains the product of two coordinate balls of half its radius, so this is F3's topology. A q-Cauchy sequence is Cauchy in both coordinates; its coordinate limits exist and converge in q by addition of the two distance bounds. The countable set $D\times E$ meets each nonempty basic product open, so is dense. Thus the product is Polish. Iterate for finitely many factors. An empty factor gives the empty space, which has the empty complete metric and empty dense set; the product of no factors is a singleton with zero metric.

For a closed $Y\subseteq X$, a Cauchy sequence in the restricted complete metric converges in $X$; its limit is in $Y$, since otherwise the open complement would contain a ball eventually containing the sequence. To prove separability, enumerate an ambient countable metric basis using dense centres and positive rational radii. Its nonempty traces form a countable basis on $Y$. A1 selects a point from each such trace; the selected set is countable and meets every nonempty relative open. If $Y$ is empty no selection is needed. This proves F1 for the closed subspace.

Now let $X\mathrm{\ne }\mathrm{\varnothing }$. Fix a complete metric and a dense sequence, and put $U_{\mathrm{\varnothing }}=X$. For each nonempty open $U_s$ enumerate all balls with dense-sequence centres and positive rational radii whose closures are contained in $U_s$ and whose diameters are at most $2^{-\mathrm{\mid }s\mathrm{\mid }-1}$. They cover $U_s$: for $x\in U_s$ choose $ϵ>0$ with $B(x,ϵ)\subseteq U_s$ and small enough for the diameter bound; a dense centre sufficiently close to $x$ and a sufficiently small rational radius yield such a ball containing $x$, with its closed ball inside $B(x,ϵ)$. The family is nonempty and countable; enumerate its indices increasingly, repeating the first if the list is finite. Set these balls to be $U_{s^{⌢}n}$. Length recursion constructs all the nonempty opens with $\overline{U_{s^{⌢}n}}\subseteq U_s$.

For $a\in \mathcal{N}$, the centres of $U_{a\upharpoonright n}$ for $n\ge 1$ form a Cauchy sequence: after stage $n$ they lie in the same set of diameter at most $2^{-n}$. Completeness gives a limit $f(a)$. For every $n$, the tail lies in $U_{a\upharpoonright (n+1)}$, so the limit lies in its closure, which is contained in $U_{a\upharpoonright n}$. Shrinking diameters show this is the only point in all those opens. For each $x\in X$, recursively take the least child containing $x$, possible by their covering property; then $x$ is that branch's unique limit. Thus $f$ is onto. Inputs sharing $n$ coordinates have images in $U_{a\upharpoonright n}$ and at distance at most $2^{-n}$, proving continuity with F2's cylinders. QED.