OAI/Geometry/SurfaceImmersion/Whitney/CrosscapNormalDefect.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual crosscap pair is exactly the zero set of a smooth normal-defect map on one open rectangle.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CrosscapCoordinateStrip.normal_defect_two_zeros line 17