Euclidean borel spaces are standard borel

For $n\ge 1$, [F1] supplies the metric. A d-infinity Cauchy sequence is Cauchy in each coordinate since $\mathrm{\mid }{x}_i-y_i\mathrm{\mid }\le d_{\mathrm{\infty }}(x,y)$. The coordinate limits exist by [F2]. For a fixed tolerance take the maximum of the finitely many coordinate convergence thresholds; beyond it all coordinate errors are below that tolerance, so the vectors converge in d-infinity. This metric induces the usual Euclidean topology: $d_{\mathrm{\infty }}\le d_2\le \sqrt{n}{d}_{\mathrm{\infty }}$ follows by bounding each squared coordinate by the maximum squared.

Induction using [F3]–[F4] makes ${\mathbb{Q}}^n$ countable. Given a vector x and positive epsilon, [F5] gives a rational in each of its finitely many coordinate intervals of radius epsilon; the resulting vector q satisfies $d_{\mathrm{\infty }}(x,q)<\epsilon$. Hence Q to the nth power is dense. For instance in dimension two, $d_{\mathrm{\infty }}((0,1),(1\mathrm{/}3,4\mathrm{/}3))=1\mathrm{/}3$.

Steps 1.1–1.2 and [F6] show R to the nth power is Polish. The identity is the presentation of [F7]. For n=0 there is just the empty tuple, with zero metric and itself as a finite dense set; it is complete and Polish. No maximum over an empty index set is used.