OAI/Geometry/SurfaceImmersion/Whitney/RulingHomotopy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The ruled deformation keeps the derivative-direction jets on the entire axis and isolates each endpoint uniformly in its time parameter.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rulingHomotopy line 14
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rulingHomotopy_smooth line 17
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rulingHomotopy_axis line 21
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rulingHomotopy_first_jet line 25
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rulingHomotopy_direction_jet line 32
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rulingHomotopy_derivative_continuous line 43
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rulingHomotopy_direction_derivative_continuous line 48
  8. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.rulingHomotopy_crosscap_isolation line 62