OAI/Geometry/SurfaceImmersion/Whitney/FiniteArcPieces.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite compact arc cover yields finitely many pairwise disjoint connected open pieces after its finite vertices are deleted.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finite_arc_pieces line 13