OAI/Geometry/SurfaceImmersion/Primitive/LoopCompactNormalMargin.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A single positive normal margin for the whole compact set of admissible low jets, before choosing a slow map or a fast scale.

  1. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.compact_normal_margin line 15