Theorems · Definition · differential geometry

EMetricSpace.ofRiemannianMetric

{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

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 286 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceBundle.RiemannianBundleIsManifoldIsContinuousRiemannianBundleT3Space