OAI/Geometry/SurfaceImmersion/Whitney/SurfaceArcTimeCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local surface coordinates with the fixed global arc-time function as the second coordinate and with the arc as the zero transverse axis.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.surface_arc_time_coordinates line 16