OAI/Geometry/SurfaceImmersion/Atlas/PlaneCurveCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual local coordinates straightening a regular curve in the surface plane.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.planeCurveTube line 13
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.planeCurveTube_smooth line 15
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.planeCurveTube_fderiv line 19
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.plane_curve_coordinates line 31