ManifoldWithCorners.metrizableSpace

theorem ManifoldWithCorners.metrizableSpace : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] {H : Type u_2} [inst_3 : TopologicalSpace H], ModelWithCorners ℝ E H → ∀ (M : Type u_3) [inst : TopologicalSpace M] [inst_4 : ChartedSpace H M] [inst_5 : SigmaCompactSpace M] [inst_6 : T2Space M], TopologicalSpace.MetrizableSpace M

This theorem states that if we have a σ-compact Hausdorff topological manifold, structured over a finite dimensional real vector space with a normed additive commutative group structure and normed space structure, then it is metrizable. In other words, we can define a metric on this manifold such that the topology it induces is the same as the original topology. The manifold is equipped with a model with corners, which provides a way to chart or parameterize the manifold. The manifold is also assumed to be σ-compact, meaning it can be expressed as the countable union of compact subsets, and is a Hausdorff space, meaning any two distinct points in the space can be separated by disjoint open sets.

More concisely: A σ-compact Hausdorff topological manifold over a finite dimensional real vector space with a normed additive commutative group structure and normed space structure is metrizable.