OAI/Geometry/SurfaceImmersion/Primitive/RegularCurveLoopRemoval.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite loop removal for a compact regular curve. The selected embedded path uses only its original image and retains a finite smooth decomposition.

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