OAI/Geometry/SurfaceImmersion/Whitney/CrosscapEndArcs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Choose disjoint initial and terminal smooth pieces of the actual crosscap-connecting arc, retaining genuine double-locus germs at their inner ends.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscap_end_arcs_regular line 16
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscap_end_arcs line 107