Theorems · Theorem · general topology

Manifold.metrizableSpace

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [inst_3 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [inst : 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.

Defined in

Mathlib.Geometry.Manifold.Metrizable

Cited by

0 results in Mathlib

Foundations

Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalTopologicalSpaceTopologicalSpaceChartedSpaceSigmaCompactSpaceT2Space