Metrizability of a σ-compact manifold

In this file we show that a σ-compact Hausdorff topological manifold over a finite-dimensional real vector space is metrizable.

theorem Manifold.metrizableSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [SigmaCompactSpace M] [T2Space M] : TopologicalSpace.MetrizableSpace M

A σ-compact Hausdorff topological manifold over a finite-dimensional real vector space is metrizable.