OAI/Geometry/SurfaceImmersion/Whitney/CollarVelocityClock.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The explicit positive change of angular variable for the collar arc.

  1. def OAI.ClosedSurfaceR4.CollarVelocity.clock line 12
  2. lemma OAI.ClosedSurfaceR4.CollarVelocity.density_eq line 14
  3. lemma OAI.ClosedSurfaceR4.CollarVelocity.hasDerivAt_clock line 22
  4. lemma OAI.ClosedSurfaceR4.CollarVelocity.clock_strictMono line 32
  5. lemma OAI.ClosedSurfaceR4.CollarVelocity.clock_continuous line 38
  6. lemma OAI.ClosedSurfaceR4.CollarVelocity.clock_period line 41
  7. lemma OAI.ClosedSurfaceR4.CollarVelocity.clock_displacement_bound line 47
  8. lemma OAI.ClosedSurfaceR4.CollarVelocity.clock_surjective line 53