Theorems · Inductive type · differential geometry

IsRiemannianManifold

{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] →
                [PseudoEMetricSpace M] →
                  [inst_5 : ChartedSpace H M] → [Bundle.RiemannianBundle fun x => TangentSpace I x] → Prop

Consider a manifold in which the tangent spaces are already endowed with an inner product, and the space is already endowed with an extended distance. We say that this is a Riemannian manifold if the distance is given by the infimum of the lengths of C^1 paths, measured using the norm in the tangent spaces. This is a Prop-valued typeclass, on top of existing data. If you need to construct a distance using a Riemannian structure, see EMetricSpace.ofRiemannianMetric.

Defined in

Mathlib.Geometry.Manifold.Riemannian.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpacePseudoEMetricSpaceChartedSpaceBundle.RiemannianBundle