OAI/Geometry/SurfaceImmersion/Whitney/CollarVelocityAngle.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The explicit collar arc has exactly two stationary angular positions.

  1. def OAI.ClosedSurfaceR4.CollarVelocity.baseAngle line 11
  2. def OAI.ClosedSurfaceR4.CollarVelocity.angle line 12
  3. lemma OAI.ClosedSurfaceR4.CollarVelocity.baseAngle_smooth line 14
  4. lemma OAI.ClosedSurfaceR4.CollarVelocity.angle_smooth line 17
  5. lemma OAI.ClosedSurfaceR4.CollarVelocity.cos_baseAngle line 20
  6. lemma OAI.ClosedSurfaceR4.CollarVelocity.sin_baseAngle line 26
  7. lemma OAI.ClosedSurfaceR4.CollarVelocity.cos_angle line 34
  8. lemma OAI.ClosedSurfaceR4.CollarVelocity.sin_angle line 37
  9. lemma OAI.ClosedSurfaceR4.CollarVelocity.hasDerivAt_baseAngle line 40
  10. lemma OAI.ClosedSurfaceR4.CollarVelocity.hasDerivAt_inverseClock line 46
  11. lemma OAI.ClosedSurfaceR4.CollarVelocity.deriv_angle line 60
  12. lemma OAI.ClosedSurfaceR4.CollarVelocity.deriv_angle_eq_zero_iff line 68