OrientationCoverMetric.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual pullback Riemannian metric on the orientation cover.

theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_bilinear_coordinates line 20
def OAI.PositiveEinsteinFour.Geometry.orientationCoverMetric line 65
Source documentation
In the preferred coordinates the derivative of the covering projection is identity, so the pullback inner product is the actual base inner product.
```
def orientationCoverMetric (g : SmoothMetric M) : SmoothMetric (OrientationCover M) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrientationCover
theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverMetric_inner line 80
theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverMetric_pullback line 83