OAI/Geometry/EinsteinFour/OrientationCoverLocalIsometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The covering projection preserves the actual local metric matrices.

  1. theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_inverse_chart_mfderiv line 18

    Source documentation

    The inverse sheet chart has the same derivative as the inverse base chart.

    theorem orientationCover_inverse_chart_mfderiv (x : OrientationCover M) {z : FourSpace}
    (hz : z ∈ (chartAt FourSpace x).target) :
    mfderiv I4 I4 (chartAt FourSpace x).symm z =
      mfderiv I4 I4 (chartAt FourSpace x.proj).symm z := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.OrientationCover

  2. theorem OAI.PositiveEinsteinFour.Geometry.metricInChart_orientationCoverMetric line 33