OAI/Geometry/SurfaceImmersion/Whitney/DoubleCurveVelocities.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

At two regular sheets the smooth paired double curve projects to regular curves on both sheets. Equal image velocities supply the key relation.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.equal_image_curve_derivatives line 13
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.paired_injective_of_equal_images line 29
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.regular_double_curve_velocities line 56