Theorems · Definition · differential geometry

IsRiemannianManifold.casesOn

{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 : PseudoEMetricSpace M] →
                  [inst_5 : ChartedSpace H M] →
                    [inst_6 : Bundle.RiemannianBundle fun x => TangentSpace I x] →
                      {motive : IsRiemannianManifold I M → Sort u} →
                        (t : IsRiemannianManifold I M) →
                          ((out : ∀ (x y : M), edist x y = Manifold.riemannianEDist I x y) → motive ⋯) → motive t

Defined in

Mathlib.Geometry.Manifold.Riemannian.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpacePseudoEMetricSpaceChartedSpaceBundle.RiemannianBundle