Theorems · Definition · differential geometry

Manifold.riemannianEDist

{E : Type u_4} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_5} →
        [inst_2 : TopologicalSpace H] →
          (I : ModelWithCorners ℝ E H) →
            {M : Type u_6} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] → [(x : M) → ENorm (TangentSpace I x)] → M → M → ENNReal

The Riemannian extended distance between two points, in a manifold where the tangent spaces have an extended norm, defined as the infimum of the lengths of C^1 paths between the points.

Defined in

Mathlib.Geometry.Manifold.Riemannian.PathELength

Cited by

14 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceENorm