Theorems · Definition · differential geometry

PseudoEMetricSpace.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] →
                        [RegularSpace M] → PseudoEMetricSpace M

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.

Defined in

Mathlib.Geometry.Manifold.Riemannian.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceBundle.RiemannianBundleIsManifoldIsContinuousRiemannianBundleRegularSpace