Milnor: a separable topological manifold has the homotopy type of a countable CW complex

Let $X$ be a Hausdorff, second countable topological space with a charted-space structure modelled on $\mathbb R^n$, i.e. a separable metrizable topological $n$-manifold (without boundary, $n\ge0$ arbitrary). Then there is a Hausdorff space $Y$ carrying the structure of a CW complex with countably many cells in each dimension, together with a homotopy equivalence

This is Milnor's theorem that a separable metric ANR — in particular any separable topological manifold — has the homotopy type of a countable CW complex (Milnor 1959, Corollary 1 to Theorem 1; the manifold case is stated explicitly there). It is the bridge that makes Whitehead's theorem available for manifolds: homotopy-theoretic statements about CW complexes (such as "weakly contractible implies contractible") transfer to manifolds along this homotopy equivalence. Second countability is essential: the long line is a Hausdorff $1$-manifold which is not of the homotopy type of any CW complex.

Formalization Note The manifold hypothesis is ChartedSpace (EuclideanSpace ℝ (Fin n)) X with T2Space X and SecondCountableTopology X; no smooth structure is involved. The CW complex is Mathlib's Topology.CWComplex (Set.univ : Set Y) (Whitehead's classical definition, on the whole space $Y$), with T2Space Y required separately since Mathlib's class does not include the Hausdorff condition, and countability is ∀ m, Countable (h.cell m) for the cell-index types of the structure h. The homotopy equivalence is ContinuousMap.HomotopyEquiv X Y, and $Y$ is taken in the same universe as $X$.