OAI/Geometry/SurfaceImmersion/Primitive/SurfaceCurveCrossingLoop.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One supported loop preserves a finite family of later curves. The boundary collars are fixed before selecting the compact interior and the large transverse derivative.

  1. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.actual_supported_curve_crossing_loop line 20