OAI/Geometry/IsometricImmersion/Immersions/NormalField.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.ambientCross line 13
  2. theorem OAI.SmoothLocal.Geometry.ambientCross_inner_left line 16
  3. theorem OAI.SmoothLocal.Geometry.ambientCross_inner_right line 21
  4. theorem OAI.SmoothLocal.Geometry.ambientCross_ne_zero_of_independent line 26
  5. theorem OAI.SmoothLocal.Geometry.ambientCross_contDiffOn line 38
  6. def OAI.SmoothLocal.Geometry.tangentCross line 53
  7. def OAI.SmoothLocal.Geometry.unitNormalField line 56
  8. theorem OAI.SmoothLocal.Geometry.tangentCross_ne_zero line 61
  9. theorem OAI.SmoothLocal.Geometry.tangentCross_contDiffOn line 66
  10. theorem OAI.SmoothLocal.Geometry.unitNormalField_norm line 70
  11. theorem OAI.SmoothLocal.Geometry.unitNormalField_inner_self line 74
  12. theorem OAI.SmoothLocal.Geometry.unitNormalField_inner_coordPartial line 78
  13. theorem OAI.SmoothLocal.Geometry.unitNormalField_isUnitNormalAt line 90
  14. theorem OAI.SmoothLocal.Geometry.unitNormalField_contDiffOn line 106
  15. theorem OAI.SmoothLocal.Geometry.exists_smooth_unitNormalField line 113