OAI/Geometry/SurfaceImmersion/Whitney/SurfaceBoundaryCollar.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Apply the zero-amplitude collar estimate to the actual immersion and its preferred jet frame.

  1. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.surfaceFrozenFirst line 14
  2. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.surfaceFrozenSize line 20
  3. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.surface_zero_amplitude_collar line 25