Theorems · Theorem · differential geometry

eventually_riemannianEDist_le_edist_extChartAt

∀ {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] (x : M),
  ∃ C > 0, ∀ᶠ (y : M) in nhds x, Manifold.riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)

Around any point x, the Riemannian distance between two points is controlled by the distance in the extended chart. In other words, the extended chart is locally Lipschitz.

Defined in

Mathlib.Geometry.Manifold.Riemannian.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceBundle.RiemannianBundleIsManifoldIsContinuousRiemannianBundle