OAI/Geometry/SurfaceImmersion/Whitney/FiniteCurveArcCover.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compactness reduces the actual local line and half-line charts to a finite cover by compact embedded arcs with open interiors.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finite_curve_arc_cover line 12