Theorems · Definition · differential geometry

PseudoEmetricSpace.ofRiemannianMetric

Deprecated since 2026-01-08Use PseudoEMetricSpace.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] →
                        [RegularSpace M] → PseudoEMetricSpace M

Alias of PseudoEMetricSpace.ofRiemannianMetric. 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 285 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceBundle.RiemannianBundleIsManifoldIsContinuousRiemannianBundleRegularSpace