OAI/Geometry/SurfaceImmersion/Whitney/RegularPathCornerPieces.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

At each interior parameter, a finite interval cover supplies actual regular smooth pieces on both sides, including their common endpoint.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCover.one_sided_intervals line 17
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCover.nonzero_slope_on_interval line 41
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCover.one_sided_regular_pieces line 53