OAI/Geometry/SurfaceImmersion/Whitney/CrosscapFormalPair.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The compact formal differential is constructed from the actual map and its crosscap strip. All exterior derivatives remain exact.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CrosscapCoordinateStrip.formal_pair line 18