OAI/Geometry/SurfaceImmersion/Whitney/ZeroAmplitudeCollar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The old ordered boundary inequality gives one uniform small-angle collar before any loop or large transverse derivative is chosen.

  1. theorem OAI.ClosedSurfaceR4.VelocityFrame.zero_amplitude_invariant_collar line 15