OAI/Geometry/SurfaceImmersion/Whitney/RegularPathEndpointPieces.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The first and last pieces of a finite embedded regular path give actual regular smooth germs even at the two endpoints.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCover.first_interval line 17
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCover.last_interval line 30
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCover.first_regular_piece line 43
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCover.last_regular_piece line 56