OAI/Geometry/SurfaceImmersion/Primitive/AnalyticCurveCrossingLoop.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Retain the finite-curve and crossing conclusions while restricting to the low-jet domain required by the exact primitive construction.

  1. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.actual_analytic_curve_crossing_loop line 17