OAI/Geometry/SurfaceImmersion/Whitney/InteriorRulingSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A compact longitudinal cutoff in the regular interior has a fixed compact regular rectangle containing all sufficiently narrow corrections.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CrosscapCoordinateStrip.interior_ruling_support line 16