OAI/Geometry/IsometricImmersion/Coordinates/OrientationNet.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothLocal.Geometry.PlanarAxis line 16
  2. def OAI.SmoothLocal.Geometry.axisRotation line 18
  3. theorem OAI.SmoothLocal.Geometry.axisRotation_yaxis line 21
  4. theorem OAI.SmoothLocal.Geometry.planarAxis_sq_sum line 27
  5. theorem OAI.SmoothLocal.Geometry.axisRotation_transpose_mul line 32
  6. theorem OAI.SmoothLocal.Geometry.axisRotation_mul_transpose line 40
  7. theorem OAI.SmoothLocal.Geometry.axisRotation_det line 48
  8. theorem OAI.SmoothLocal.Geometry.exists_finite_unit_axis_net line 54
  9. def OAI.SmoothLocal.Geometry.orientationAxes line 72
  10. theorem OAI.SmoothLocal.Geometry.orientationAxes_unit line 74
  11. theorem OAI.SmoothLocal.Geometry.orientationAxes_cover line 77
  12. def OAI.SmoothLocal.Geometry.orientationRotations line 81
  13. theorem OAI.SmoothLocal.Geometry.orientationRotations_properties line 85
  14. theorem OAI.SmoothLocal.Geometry.orientationRotations_cover line 93