OAI/Geometry/Immersion/ClosedSurface/ChartModel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClosedSurfaceR4.planeCoordinates line 13
  2. def OAI.ClosedSurfaceR4.spaceCoordinates line 16
  3. def OAI.ClosedSurfaceR4.coordinateDomain line 20
  4. def OAI.ClosedSurfaceR4.coordinateCenter line 23
  5. def OAI.ClosedSurfaceR4.coordinateMap line 25
  6. lemma OAI.ClosedSurfaceR4.coordinateDomain_open line 28
  7. lemma OAI.ClosedSurfaceR4.coordinateCenter_mem line 32
  8. lemma OAI.ClosedSurfaceR4.coordinateMap_at_center line 35
  9. lemma OAI.ClosedSurfaceR4.coordinateMap_smoothOn line 39
  10. lemma OAI.ClosedSurfaceR4.mfderiv_coordinateMap_center line 49
  11. lemma OAI.ClosedSurfaceR4.coordinateMap_immersion_center line 77
  12. lemma OAI.ClosedSurfaceR4.spaceCoordinates_dot line 84
  13. lemma OAI.ClosedSurfaceR4.coordinateMetric_at_center line 88