English
Given a Riemannian metric on a manifold, one constructs a canonical pseudo-emetric space structure on the manifold whose topology matches the original one.
Русский
Для данного римманова метрического пространства над многообразием строится каноническая структура псевдомерического пространства, топология которого совпадает с исходной.
LaTeX
$$$$\\text{ofRiemannianMetric}(I,M): \\text{PseudoEmetricSpace } M.$$$$
Lean4
/-- The pseudoemetric 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 [RegularSpace M] : PseudoEMetricSpace M :=
PseudoEmetricSpace.ofEdistOfTopology (riemannianEDist I (M := M)) (fun _ ↦ riemannianEDist_self)
(fun _ _ ↦ riemannianEDist_comm) (fun _ _ _ ↦ riemannianEDist_triangle)
(fun x ↦
(basis_sets (𝓝 x)).to_hasBasis' (fun _ hs ↦ setOf_riemannianEDist_lt_subset_nhds' I hs)
(fun _ hc ↦ eventually_riemannianEDist_lt I x hc))
