OAI/Geometry/SurfaceImmersion/Whitney/CrosscapArcGermRestriction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The same embedded connecting arc and exact parameter germs survive a regular-locus-preserving change fixed near its singular endpoints.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CrosscapConnectingArc.restrict_germs line 16