Standard borel spaces admit bimeasurable real codings

If $E=\mathrm{\varnothing }$, the empty bijection onto $\mathrm{\varnothing }$ is bimeasurable. Otherwise fix the single Polish presentation $h:E\to P$ of [F1]. Its separability and metrizability give a homeomorphic embedding $e:P\to Q=[0,1{]}^{\mathbb{N}}$ by [F2].

The interval $[0,1]$ is complete: a Cauchy sequence converges in $\mathbb{R}$ by [F7], and its limit stays between zero and one by the limit inequalities. Its metric is bounded by one. The metric $D(x,y)={\sum }_{n\ge 0}{2}^{-(n+1)}\mathrm{\mid }{x}_n-y_n\mathrm{\mid }$ makes $Q$ a metric space by [F3]. The image $Y=e[P]$ is completely metrizable, transporting a complete compatible metric from $P$. AC supplies DC as described in [F6], so [F4] yields that $Y$ is $G_{\delta }$ and consequently Borel in $Q$. The currently repaired supplier proves the ambient equality: points in every small open neighbourhood union lie within $1\mathrm{/}n$ of $Y$, hence in its closure, before the complete-metric limit argument.

Let $c:Q\to C$ be [F5]. Since $c^{-1}$ is measurable, $c[Y]=(c^{-1}{)}^{-1}[Y]$ is Borel in $C$, and therefore in $[0,1]$, because $C$ itself is Borel. Restricting $c$ and its inverse to $Y$ and $c[Y]$ preserves measurability. The homeomorphism $e$ is bimeasurable on trace Borel sets. Thus $c\circ e\circ h$ and $h^{-1}\circ e^{-1}\circ c^{-1}$ are mutually inverse measurable maps between $E$ and $c[Y]$.