Under the Axiom of Choice, a space is Polish exactly when it is homeomorphic to a $G_{\delta }$ subspace of the Hilbert cube

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

Every separable metrizable space is homeomorphic to a subspace of the Hilbert cube $[0,1{]}^{\mathbb{N}}$. (Every separable metrizable space embeds in the Hilbert cube $[0,1{]}^{\mathbb{N}}$).

Assume the Axiom of Countable Choice. A subspace of a Polish space is Polish if and only if it is a $G_{\delta }$ subset. (Under Dependent Choice, a subspace of a Polish space is Polish exactly when it is $G_{\delta }$).

Let $((X_n,d_n){)}_{n\in \mathbb{N}}$ be complete metric spaces with $d_n\le 1$. On ${\prod }_n{X}_n$, the formula $D(x,y)={\sum }_{n=0}^{\mathrm{\infty }}{2}^{-(n+1)}{d}_n(x_n,y_n)$ defines a complete metric inducing the product topology. The empty product is the one-point space. (The standard weighted metric on a countable product of bounded complete metric spaces is complete).

Assume the Axiom of Choice (def-axiom-of-choice). Let $I$ be a set and let $(X_i,{\mathcal{T}}_i{)}_{i\in I}$ be a family of compact topological spaces (def-compact-space, def-topological-space). Then the product $P:={\prod }_{i\in I}{X}_i$ with the product topology (def-product-topology) is compact. The Axiom of Choice is spent twice, and both uses are flagged below. Once inside thm-alexander-subbase-lemma, through Zorn's lemma (thm-zorn), and once directly at step 2.1, to produce a point of a product of nonempty sets. (Tychonoff's theorem: an arbitrary product of compact spaces is compact in the product topology, assuming the Axiom of Choice).