OAI/Geometry/IsometricImmersion/Metric.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothLocal.Geometry.Ambient line 11

    Also declared: ComparatorChallenges/IsometricImmersion.lean:17 (same declaration text).

  2. abbrev OAI.SmoothLocal.Geometry.MetricField line 12
  3. def OAI.SmoothLocal.Geometry.square line 14

    Also declared: ComparatorChallenges/IsometricImmersion.lean:19 (same declaration text).

  4. def OAI.SmoothLocal.Geometry.SmoothPositiveOn line 16
  5. def OAI.SmoothLocal.Geometry.IsometricOn line 19
  6. def OAI.SmoothLocal.Geometry.inverseMetric line 23
  7. def OAI.SmoothLocal.Geometry.christoffel line 25
  8. def OAI.SmoothLocal.Geometry.covHessian line 30
  9. def OAI.SmoothLocal.Geometry.covectorNormSq line 34
  10. def OAI.SmoothLocal.Geometry.riemann line 37
  11. def OAI.SmoothLocal.Geometry.gaussianCurvature line 42
  12. def OAI.SmoothLocal.Geometry.height line 45
  13. def OAI.SmoothLocal.Geometry.secondFundamental line 48
  14. theorem OAI.SmoothLocal.Geometry.isometricOn_injective_differential line 52
  15. def OAI.SmoothLocal.Geometry.MainTarget line 66