Representation of Polish metric spaces

In this chapter we develop the so-called standard representation of complete separable metric spaces X, so-called ‘Polish’ metric spaces. Via this representation, elements of X are represented by number theoretic functions, i.e. objects f of type-1. Moreover, we will show that the representation can be arranged in such a way that every function f¹ represents a unique element in X. In general, an element in X will have many representatives f. On the representatives we define an equivalence relation f₁= _X f₂:≡ (f₁,f₂ represent the same X-element). Instead of having explicitly to introduce elements of X as equivalence classes of representatives, we can use the representatives themselves and then state that the function or predicate in question respects the equivalence relations. E.g. a function F:X→Y between two Polish spaces represented in this way is just a functional Φ¹⁽¹⁾ satisfying

$$\forall f^{1}_{1},f^{1}_{2}(f_{1}=_{X}f_{2}\rightarrow \Phi(f_{1})=_{Y}\Phi (f_{2})).$$

For compact metric spaces K we can arrange that the elements x∈K are represented already by functions f≤₁M which are bounded by a fixed function M depending on K only. This representation goes back to L.E.J. Brouwer (see also the historical comments at the end of this chapter). Again we can achieve that every f≤₁M represents a unique element in K.