OAI/Geometry/SurfaceImmersion/Whitney/LocalDoubleCurveLift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A curve locally in the double locus has a continuous local lift to its actual subtype, with an arbitrary fixed continuation outside the germ.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.local_double_curve_lift line 14