OAI/Geometry/SurfaceImmersion/Primitive/ActualSupportedSurfaceLoop.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Construct a supported periodic surface loop from an actual immersion, a preferred normal, a positive phase Hessian and the prescribed amplitude.

  1. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.actual_supported_surface_loop line 13