OAI/Geometry/SurfaceImmersion/Atlas/TriangularTimeCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Replacing the longitudinal coordinate by a smooth function with unit axial derivative is an actual local plane diffeomorphism.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.timeCoordinateMap line 14
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.timeCoordinateMap_smooth line 16
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.timeCoordinateMap_regular line 24
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.triangular_time_coordinates line 56