OAI/Geometry/SurfaceImmersion/Primitive/UniformTransverseProfiles.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual primitive's transverse first and second derivatives approach the slow baseline uniformly over all maps in the fixed compact jet domain.

  1. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.uniform_transverse_profiles line 16