OAI/Geometry/SurfaceImmersion/Primitive/SurfaceFiniteCurveLoop.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_finite_curve_loop line 19