OAI/Geometry/IsometricImmersion/Metrics/WarpedMetric.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.warpedMetric line 15
  2. theorem OAI.SmoothLocal.Geometry.warpedMetric_00 line 18
  3. theorem OAI.SmoothLocal.Geometry.warpedMetric_01 line 21
  4. theorem OAI.SmoothLocal.Geometry.warpedMetric_10 line 24
  5. theorem OAI.SmoothLocal.Geometry.warpedMetric_11 line 27
  6. theorem OAI.SmoothLocal.Geometry.warpedMetric_det line 30
  7. theorem OAI.SmoothLocal.Geometry.warpedMetric_smoothPositiveOn line 34
  8. theorem OAI.SmoothLocal.Geometry.inverseMetric_warpedMetric line 51
  9. theorem OAI.SmoothLocal.Geometry.coordPartial_const line 58
  10. theorem OAI.SmoothLocal.Geometry.coordPartial_mul line 62
  11. theorem OAI.SmoothLocal.Geometry.coordPartial_neg line 68
  12. theorem OAI.SmoothLocal.Geometry.coordPartial_sq line 72
  13. theorem OAI.SmoothLocal.Geometry.coordPartial_warpedMetric line 79
  14. def OAI.SmoothLocal.Geometry.warpedChristoffel line 85
  15. theorem OAI.SmoothLocal.Geometry.christoffel_warpedMetric line 92
  16. theorem OAI.SmoothLocal.Geometry.christoffel_warpedMetric_111 line 100
  17. theorem OAI.SmoothLocal.Geometry.riemann_warpedMetric_0101 line 105
  18. theorem OAI.SmoothLocal.Geometry.gaussianCurvature_warpedMetric line 140