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]
:
A σ-compact Hausdorff topological manifold over a finite dimensional real vector space is metrizable.
@[deprecated Manifold.metrizableSpace (since := "2024-11-11")]
theorem
ManifoldWithCorners.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]
:
Alias of Manifold.metrizableSpace.
A σ-compact Hausdorff topological manifold over a finite dimensional real vector space is metrizable.