OAI/Geometry/Immersion/ClosedSurface/MetricPullback.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClosedSurfaceR4.coordinateInverse line 16
  2. lemma OAI.ClosedSurfaceR4.coordinateInverse_smoothOn line 19
  3. lemma OAI.ClosedSurfaceR4.coordinateInverse_center line 25
  4. def OAI.ClosedSurfaceR4.metricPullback line 28
  5. lemma OAI.ClosedSurfaceR4.metricPullback_continuousOn line 32
  6. lemma OAI.ClosedSurfaceR4.metricPullback_pos line 52
  7. lemma OAI.ClosedSurfaceR4.mfderiv_coordinateInverse_center line 61
  8. def OAI.ClosedSurfaceR4.coordinateMetric line 85
  9. lemma OAI.ClosedSurfaceR4.coordinateMetric_continuousAt_center line 89
  10. lemma OAI.ClosedSurfaceR4.coordinateMetric_evaluate line 97
  11. lemma OAI.ClosedSurfaceR4.tensor_positive_iff line 118
  12. lemma OAI.ClosedSurfaceR4.coordinateMetric_positive_center line 153