OAI/Geometry/SurfaceImmersion/Whitney/CollarVelocityInverse.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Smooth parameter dependence of the explicit collar clock's inverse.

  1. lemma OAI.ClosedSurfaceR4.CollarVelocity.clock_smooth line 12
  2. def OAI.ClosedSurfaceR4.CollarVelocity.inverseClock line 20
  3. lemma OAI.ClosedSurfaceR4.CollarVelocity.clock_inverseClock line 22
  4. lemma OAI.ClosedSurfaceR4.CollarVelocity.inverseClock_clock line 25
  5. lemma OAI.ClosedSurfaceR4.CollarVelocity.clock_zero line 28
  6. lemma OAI.ClosedSurfaceR4.CollarVelocity.inverseClock_zero line 29
  7. lemma OAI.ClosedSurfaceR4.CollarVelocity.inverseClock_period line 32
  8. def OAI.ClosedSurfaceR4.CollarVelocity.equation line 37
  9. lemma OAI.ClosedSurfaceR4.CollarVelocity.equation_smooth line 39
  10. lemma OAI.ClosedSurfaceR4.CollarVelocity.equation_partial line 42
  11. lemma OAI.ClosedSurfaceR4.CollarVelocity.equation_partial_invertible line 53
  12. lemma OAI.ClosedSurfaceR4.CollarVelocity.inverseClock_smooth line 63