English
A σ-compact Hausdorff topological manifold modeled on a finite-dimensional real vector space is metrizable.
Русский
σ-компактное хаусдорфово топологическое многообразие, моделируемое на конечномерном вещественном векторном пространстве, метризуемо.
LaTeX
$$$\\exists d: M \\times M \\to \\mathbb{R}_{\\ge 0},\\; d\\text{ является метрикой на }M$$$
Lean4
/-- A σ-compact Hausdorff topological manifold over a finite-dimensional real vector space is
metrizable. -/
theorem metrizableSpace {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type*}
[TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type*) [TopologicalSpace M] [ChartedSpace H M]
[SigmaCompactSpace M] [T2Space M] : MetrizableSpace M :=
by
haveI := I.locallyCompactSpace; haveI := ChartedSpace.locallyCompactSpace H M
haveI := I.secondCountableTopology
haveI := ChartedSpace.secondCountable_of_sigmaCompact H M
exact metrizableSpace_of_t3_secondCountable M
