OAI/Geometry/IsometricImmersion/Curvature/MetricCurvatureJet.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothLocal.Geometry.MetricMatrix line 11
  2. abbrev OAI.SmoothLocal.Geometry.MetricFirstJet line 12
  3. abbrev OAI.SmoothLocal.Geometry.MetricSecondJet line 13
  4. def OAI.SmoothLocal.Geometry.inverseDerivativeJet line 15
  5. def OAI.SmoothLocal.Geometry.christoffelJet line 19
  6. def OAI.SmoothLocal.Geometry.christoffelDerivativeJet line 22
  7. def OAI.SmoothLocal.Geometry.riemannJet line 28
  8. def OAI.SmoothLocal.Geometry.curvatureJet line 35
  9. theorem OAI.SmoothLocal.Geometry.inverseMetric_coordPartial_eq_jet line 38
  10. theorem OAI.SmoothLocal.Geometry.gaussianCurvature_eq_curvatureJet line 68
  11. theorem OAI.SmoothLocal.Geometry.metricMatrix_inverse_continuousAt line 89
  12. theorem OAI.SmoothLocal.Geometry.inverseDerivativeJet_continuousAt line 109
  13. theorem OAI.SmoothLocal.Geometry.christoffelJet_continuousAt line 118
  14. theorem OAI.SmoothLocal.Geometry.christoffelDerivativeJet_continuousAt line 127
  15. theorem OAI.SmoothLocal.Geometry.riemannJet_continuousAt line 138
  16. theorem OAI.SmoothLocal.Geometry.curvatureJet_continuousAt line 149