English
The emetric space structure associated to a Riemannian metric is defined and agrees with the original topology when the base space is regular.
Русский
Структура эмитрического пространства, ассоциированная с риммановой метрикой, задаётся и совпадает с исходной топологией на регулярном пространстве.
LaTeX
$$$$\\text{ofRiemannianMetric} \\Rightarrow \\text{EMetricSpace on }M.$$$$
Lean4
/-- The emetric space structure associated to a Riemannian metric on a manifold. Designed
so that the topology is defeq to the original one.
This should only be used when constructing data in specific situations. To develop the theory,
one should rather assume that there is an already existing emetric space structure, which satisfies
additionally the predicate `IsRiemannianManifold I M`. -/
@[reducible]
def ofRiemannianMetric [T3Space M] : EMetricSpace M :=
letI : PseudoEMetricSpace M := PseudoEmetricSpace.ofRiemannianMetric I M
EMetricSpace.ofT0PseudoEMetricSpace M
