OAI/Geometry/SurfaceImmersion/Whitney/RuledCrosscapStrip.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One rectangular neighborhood works throughout the actual ruled homotopy: its singular set is exactly the original two endpoints.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CrosscapCoordinateStrip.ruled_neighborhood line 17
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CrosscapCoordinateStrip.ruled_rectangle line 96