OAI/Geometry/SurfaceImmersion/Whitney/OrientedDoubleChartArc.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual smooth regular embedded arc pieces in the double locus, with the image and endpoint order of the original topological arc.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothDoubleChart.oriented_arc line 16