OAI/Geometry/SurfaceImmersion/Primitive/ProjectedVelocityFrame.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual frame formed from the projected tangent and preferred normal.

  1. def OAI.ClosedSurfaceR4.VelocityFrame.projectedFirst line 13
  2. def OAI.ClosedSurfaceR4.VelocityFrame.projectedSecond line 16
  3. lemma OAI.ClosedSurfaceR4.VelocityFrame.projected_blend_nonzero line 19
  4. theorem OAI.ClosedSurfaceR4.VelocityFrame.projected_frame_orthonormal line 43
  5. lemma OAI.ClosedSurfaceR4.VelocityFrame.projectedFirst_zero line 55
  6. lemma OAI.ClosedSurfaceR4.VelocityFrame.projectedFirst_one line 59
  7. theorem OAI.ClosedSurfaceR4.VelocityFrame.projected_frame_smoothOn line 65