OAI/Geometry/SurfaceImmersion/Whitney/OrderedArcSeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Consecutive subarcs of an embedded arc have disjoint interiors. This supplies the separation needed by the smooth joining operation.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ordered_arc_images_separated line 14