[Math] Is the space of continuous functions from a compact metric space into a Polish space Polish

gn.general-topologypr.probabilityreference-request

Let $K$ be a compact metric space, and $(E,d_E)$ a complete separable metric space.
Define $C:=C(K,E)$ to be the continuous functions from $K$ to $E$ equipped with
the metric $d(f,g)=\sup_{k\in K}\ d_E (f(k),g(k))$. Is the space $C$ separable?

The result is true when $E$ is the real line; this is Corollary 11.2.5 in Dudley's
book Real Analysis and Probability.

The result is also true when $K=[0,1]$ (if I'm not being too careless) by
considering $C$ as a subspace of the Skorohod space $D_E[0,1]$, which is
complete and separable by Theorem 5.6 in Ethier and Kurtz's book Markov Processes:
Characterization and Convergence
.

For general $K$, it is not so obvious how to find an explicit countable
dense set in $C$, but I suspect one could modify Ethier and Kurtz's approach and get a proof.

But surely this result is known, and stated in some book? I've searched through
my library without success.


Update: This result is also Theorem 2.4.3 of S. M. Srivastava's book A Course on Borel Sets. His proof is the same as Kechris's. I have also found an alternative, but false, published proof using the "fact" that $C(K,E)$ is $\sigma$-compact. Beware!

Best Answer

Yes, it appears e.g. as Theorem 4.19 in Chapter I of Kechris' Classical Descriptive Set Theory. (The relevant page is visible in Google Books if it's not in your library.)