mathlib documentation

geometry.manifold.metrizable

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.

A σ-compact Hausdorff topological manifold over a finite dimensional real vector space is metrizable.