OAI/Geometry/SurfaceImmersion/Primitive/ActualAnalyticSurfaceLoop.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The constructed geometric loop in the exact coordinates and support form used by the primitive polynomial expansion.

  1. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.actual_analytic_surface_loop line 14