OAI/Geometry/SurfaceImmersion/Primitive/CrossingCoordinateMap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The explicit map straightening two transverse surface sheets that already use a common curve parameter as their second coordinate.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingCoordinateMap line 13
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingCoordinateMap_smooth line 16
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingCoordinateMap_fderiv line 22
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.common_axis_derivatives line 40
  5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingCoordinateMap_regular line 58
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingCoordinateMap_left line 67
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingCoordinateMap_right line 74