OAI/Geometry/EinsteinFour/OrientationCoverCurvature.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Curvature and Einstein normalization are preserved by the actual cover.

  1. theorem OAI.PositiveEinsteinFour.Geometry.partialDeriv_eq_of_eventuallyEq line 17
  2. theorem OAI.PositiveEinsteinFour.Geometry.christoffel_orientationCoverMetric line 22
  3. theorem OAI.PositiveEinsteinFour.Geometry.curvatureComponent_orientationCoverMetric line 33
  4. theorem OAI.PositiveEinsteinFour.Geometry.ricciInChart_orientationCoverMetric line 46
  5. theorem OAI.PositiveEinsteinFour.Geometry.sectionalNumerator_orientationCoverMetric line 51
  6. theorem OAI.PositiveEinsteinFour.Geometry.isEinstein_orientationCoverMetric line 59
  7. theorem OAI.PositiveEinsteinFour.Geometry.positive_orientationCoverMetric line 70