OAI/Geometry/SurfaceImmersion/Primitive/VelocityPlaneRays.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The boundary non-antipodality condition survives projection to the velocity plane.

  1. lemma OAI.ClosedSurfaceR4.VelocityFrame.no_opposite_ray_of_normalized line 12
  2. lemma OAI.ClosedSurfaceR4.VelocityFrame.projected_second_form line 33
  3. lemma OAI.ClosedSurfaceR4.VelocityFrame.projection_preserves_no_opposite_ray line 43
  4. lemma OAI.ClosedSurfaceR4.VelocityFrame.projected_tangent_no_opposite_ray line 65