OAI/Geometry/SurfaceImmersion/Whitney/CompactCollarJet.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Uniform injectivity of collar jets near a compact family of transverse axis frames.
- theorem
OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_collar_jetline 14