Under the Axiom of Choice, the Hilbert cube is compact, Polish, and universal for separable metrizable spaces

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

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

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

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