OAI/Geometry/SurfaceImmersion/Whitney/DoubleLocusArc.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A regular zero of the pair-chart difference map has an actual smooth, injective interval parametrization of its local zero set.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.double_locus_local_arc line 13