CrosscapEndpoint.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Each prepared crosscap has a genuine embedded half-interval neighborhood in the compactified unordered double curve.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscap_half_arc_neighborhood line 15