@[implicit_reducible]
noncomputable def
manifoldMetric
{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]
[T2Space M]
[SigmaCompactSpace M]
:
A metric defining the topology on a σ-compact T₂ real manifold.