Every compact metric space can be embedded into the Hilbert cube. #
In this file we prove exists_closed_embedding_to_hilbert: every compact metric space can be
embedded into the Hilbert cube (ℕ → unitInterval).
theorem
exists_closed_embedding_to_hilbert_cube
(X : Type u_1)
[MetricSpace X]
[CompactSpace X]
:
∃ (f : X → ℕ → ↑unitInterval), Topology.IsClosedEmbedding f
Every compact metric space can be embedded into the Hilbert cube.