OAI/Geometry/SurfaceImmersion/Whitney/DoubleCurveBoundaryArc.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every actual crosscap endpoint is joined to another one by an embedded arc of the compactified double curve, with regular interior.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.prepared_double_curve_boundary_arc line 16