Every separable metrizable space embeds in the Hilbert cube $[0,1{]}^{\mathbb{N}}$

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

A topological space $X$ is separable if some at most countable subset $D\subseteq X$ is dense in $X$ (def-dense-top, def-countable). Equivalently, every nonempty open subset of $X$ meets $D$. (Separability: the existence of an at most countable dense subset).

A topological space $(X,\mathcal{T})$ (def-topological-space) is metrizable if there is a metric $d$ on $X$ (def-metric-space) whose metric topology is $\mathcal{T}$, that is $\mathcal{T}={\mathcal{T}}_d$ (def-metric-topology). Such a $d$ is said to induce or metrise $\mathcal{T}$. (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not).

The product set. Let $I$ be a set and let $X_i$ be a set for each $i\in I$. The product is ${\prod }_{i\in I}{X}_i:=\{x:x\text{ is a function with domain }I\text{ and }x(i)\in X_i\text{ for every }i\in I\},$ and we write $x_i:=x(i)$, the $i$-th coordinate of $x$. Two elements of the product are equal exactly when they agree at every index, functions being equal when they have the same domain and the same values. For $j\in I$ the $j$-th projection is ${\pi }_j:{\prod }_{i\in I}{X}_i\to X_j,{\pi }_j(x):=x_j\mathrm{.}$. The product topology ${\mathcal{T}}^{\mathrm{\Pi }}$ on ${\prod }_i{X}_i$ is the initial topology of the projections: the topology generated by the subbasis $\{{\pi }_i^{-1}[U]:i\in I,U\in {\mathcal{T}}_i\}$. Finite intersections of subbasic sets form a basis for it, and they are exactly the boxes ${\prod }_{i\in I}{U}_i$ with every $U_i$ open in $X_i$ and $U_i=X_i$ for all but finitely many $i$. (The product set ${\prod }_{i\in I}{X}_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

Let $(X,d)$ be a metric space (def-metric-space) and define, for $x,y\in X$, $d^{\mathrm{\prime }}(x,y):=\min \{d(x,y),1\},d^{\mathrm{\prime }\mathrm{\prime }}(x,y):=\frac{d(x,y)}{1+d(x,y)}\mathrm{.}$ Both are well defined: $d(x,y)\ge 0$ (lem-metric-nonnegativity), so $1+d(x,y)>0$ and is invertible, and the minimum of a two-element set of reals exists (lem-finite-set-has-max, def-max-min). Then: 1. $d^{\mathrm{\prime }}$ and $d^{\mathrm{\prime }\mathrm{\prime }}$ are metrics on $X$. 2. $d^{\mathrm{\prime }}(x,y)\le 1$ and $d^{\mathrm{\prime }\mathrm{\prime }}(x,y)<1$ for all $x,y$; hence $(X,d^{\mathrm{\prime }})$ and $(X,d^{\mathrm{\prime }\mathrm{\prime }})$ are bounded metric spaces (def-metric-bounded-diameter), and if $X\mathrm{\ne }\mathrm{\varnothing }$ then $\mathrm{diam}(X)\le 1$ for both. 3. $d^{\mathrm{\prime }}$ and $d^{\mathrm{\prime }\mathrm{\prime }}$ are each uniformly equivalent to $d$, hence topologically equivalent to it (def-equivalent-metrics, thm-metric-equivalence-hierarchy). Consequently every metric space carries a bounded metric with exactly the same topology, so boundedness cannot be read off the topology alone. ($\min (d,1)$ and $d\mathrm{/}(1+d)$ are metrics uniformly equivalent to $d$, so every metric space carries a bounded metric with the same topology).