Theorems · Definition · differential geometry

EmetricSpace.ofRiemannianMetric

Deprecated since 2026-01-08Use EMetricSpace.ofRiemannianMetric instead.

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_2} →
        [inst_2 : TopologicalSpace H] →
          (I : ModelWithCorners ℝ E H) →
            (M : Type u_3) →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] →
                  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] →
                    [inst_6 : IsManifold I 1 M] →
                      [IsContinuousRiemannianBundle E fun x => TangentSpace I x] → [T3Space M] → EMetricSpace M

Alias of EMetricSpace.ofRiemannianMetric. 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.

Defined in

Mathlib.Geometry.Manifold.Riemannian.Basic

Cited by

0 results in Mathlib

Foundations

Depth 287 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceBundle.RiemannianBundleIsManifoldIsContinuousRiemannianBundleT3Space