OAI/Geometry/EinsteinFour/OrientationCoverProjection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The projection of the actual orientation cover is smooth and its derivative is the identity in the preferred tangent coordinates.

  1. theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_projection_inCharts line 18
  2. theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_projection_smooth line 34
  3. theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_projection_hasMFDerivAt line 44
  4. theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_projection_mfderiv line 51