OAI/Geometry/SurfaceImmersion/Primitive/CrossingNormalPath.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The preferred-normal adjustment at a crossing: a normalized straight path stays away from both forbidden antipodes and ends with positive pairings.

  1. lemma OAI.ClosedSurfaceR4.VelocityFrame.nonzero_of_dot_pos line 13
  2. lemma OAI.ClosedSurfaceR4.VelocityFrame.normalize_dot_pos line 18
  3. lemma OAI.ClosedSurfaceR4.VelocityFrame.crossing_blend_nonzero line 23
  4. theorem OAI.ClosedSurfaceR4.VelocityFrame.crossing_normal_path line 36
  5. theorem OAI.ClosedSurfaceR4.VelocityFrame.crossing_normal_path_endpoint line 58
  6. lemma OAI.ClosedSurfaceR4.VelocityFrame.crossing_normal_path_smoothAt line 68