English
For a given Riemannian metric on a manifold, the manifold is a Riemannian manifold with the corresponding distance function.
Русский
При заданной риммановой метрике над многообразием множество становится риммановым многообразием с соответствующей функцией расстояния.
LaTeX
$$$$\\text{IsRiemannianManifold}(I,M).$$$$
Lean4
/-- Given a manifold with a Riemannian metric, consider the associated Riemannian distance. Then
by definition the distance is the infimum of the length of paths between the points, i.e., the
manifold satisfies the `IsRiemannianManifold I M` predicate. -/
instance [RegularSpace M] :
letI : PseudoEMetricSpace M := PseudoEmetricSpace.ofRiemannianMetric I M
IsRiemannianManifold I M :=
by
letI : PseudoEMetricSpace M := PseudoEmetricSpace.ofRiemannianMetric I M
exact ⟨fun x y ↦ rfl⟩
