Metrizability of a σ-compact manifold #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we show that a σ-compact Hausdorff topological manifold over a finite dimensional real vector space is metrizable.
theorem
manifold_with_corners.metrizable_space
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
[finite_dimensional ℝ E]
{H : Type u_2}
[topological_space H]
(I : model_with_corners ℝ E H)
(M : Type u_3)
[topological_space M]
[charted_space H M]
[sigma_compact_space M]
[t2_space M] :
A σ-compact Hausdorff topological manifold over a finite dimensional real vector space is metrizable.