OAI/Geometry/IsometricImmersion/Immersions/BoundaryNormal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.coordinateCircle line 13
  2. def OAI.SmoothLocal.Geometry.coordinateCircleVelocity line 16
  3. theorem OAI.SmoothLocal.Geometry.coordinateCircle_contDiff line 19
  4. theorem OAI.SmoothLocal.Geometry.coordinateCircle_hasDerivAt line 31
  5. theorem OAI.SmoothLocal.Geometry.coordinateCircle_equation line 47
  6. theorem OAI.SmoothLocal.Geometry.unitNormalField_circle_hasDerivAt_zero line 60
  7. theorem OAI.SmoothLocal.Geometry.unitNormalField_circle_constant line 75
  8. theorem OAI.SmoothLocal.Geometry.height_circle_hasDerivAt_zero line 87
  9. theorem OAI.SmoothLocal.Geometry.height_circle_constant line 99
  10. theorem OAI.SmoothLocal.Geometry.exists_circle_constant_normal_and_height line 109