OAI/Geometry/SurfaceImmersion/Whitney/CalibratedCollarFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The small-angle collar is chosen before the compact interior curve set and before its turn threshold. The later translation may overlap that collar.

  1. theorem OAI.ClosedSurfaceR4.CollarVelocity.calibrated_jet_collar_family line 13