OAI/Geometry/SurfaceImmersion/Whitney/NormalLinearizationHomotopy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Linearizing only the transverse coordinate preserves exactly the two zeros on a common thin rectangle throughout the homotopy.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.plane_map_columns line 14
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalizedLinearModel_fderiv_eq line 25
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.linearDefectHomotopy line 36
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.linearDefectHomotopy_smooth line 39
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.linearDefectHomotopy_fderiv line 44
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.linearDefectHomotopy_axis line 50
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.linearDefectHomotopy_jet line 56
  8. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.linearDefectHomotopy_two_zeros line 64