OAI/Geometry/IsometricImmersion/Immersions/RankOneOrientation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.exists_nonzero_dyad_of_symmetric_rank_one line 14
  2. theorem OAI.SmoothLocal.Geometry.exists_unit_dyad_of_symmetric_rank_one line 51
  3. def OAI.SmoothLocal.Geometry.clockwiseAxis line 65
  4. theorem OAI.SmoothLocal.Geometry.planar_inner_coordinates line 67
  5. theorem OAI.SmoothLocal.Geometry.clockwiseAxis_orthogonal line 72
  6. theorem OAI.SmoothLocal.Geometry.clockwiseAxis_unit line 77
  7. theorem OAI.SmoothLocal.Geometry.nearby_axis_inner_bounds line 84
  8. def OAI.SmoothLocal.Geometry.rotatedForm line 99
  9. theorem OAI.SmoothLocal.Geometry.rotated_dyad_entries line 102
  10. theorem OAI.SmoothLocal.Geometry.rotated_dyad_admissible_axis line 112
  11. theorem OAI.SmoothLocal.Geometry.exists_orientationRotation_for_rank_one line 134