OAI/Geometry/SurfaceImmersion/Whitney/SupportedCrosscapCancellation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A compactly supported removal of the standard pair of crosscaps. The replacement is an actual smooth immersion of the coordinate plane.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_supported_crosscap_cancellation line 13