OAI/Geometry/SurfaceImmersion/Whitney/SmoothCrosscapConnectingArc.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Assemble the two actual crosscap endpoint pieces and the compact interior into one smooth regular embedded ordered connecting arc.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_crosscap_connecting_arc_endpoint_regular line 18
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_crosscap_connecting_arc line 109