OAI/Geometry/SurfaceImmersion/Whitney/SameSideCollarHomotopy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A common positive transverse functional gives an explicit regular linear homotopy of boundary vectors.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.linearTransverseHomotopy line 14
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.linearTransverseHomotopy_smooth line 17
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.same_side_collar_jet line 23