OAI/Geometry/EinsteinFour/OrientationCoverDistanceDown.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Projection preserves the length of every differentiable path, hence cannot increase the actual Riemannian distance.

  1. theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_curve_derivative line 19
  2. theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_curve_length line 29
  3. theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_distance_down line 41