OAI/Geometry/IsometricImmersion/Curvature/IntrinsicCurvature.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.metric_second_compatibility line 14
  2. def OAI.SmoothLocal.Geometry.loweredRiemann line 52
  3. theorem OAI.SmoothLocal.Geometry.loweredRiemann_skew_last line 55
  4. theorem OAI.SmoothLocal.Geometry.loweredRiemann_skew_first_add line 60
  5. theorem OAI.SmoothLocal.Geometry.loweredRiemann_skew_first line 71
  6. theorem OAI.SmoothLocal.Geometry.loweredRiemann_self_first line 77
  7. theorem OAI.SmoothLocal.Geometry.loweredRiemann_self_last line 82
  8. theorem OAI.SmoothLocal.Geometry.loweredRiemann_0101 line 87
  9. theorem OAI.SmoothLocal.Geometry.loweredRiemann_factorization line 92
  10. def OAI.SmoothLocal.Geometry.curvatureFactor line 105
  11. theorem OAI.SmoothLocal.Geometry.curvatureFactor_contDiffOn line 108
  12. theorem OAI.SmoothLocal.Geometry.riemann_factorization line 117