OAI/Geometry/SurfaceImmersion/Whitney/FiniteDoubleCurvePieces.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual compactified surface double curve has a finite vertex/ open-edge decomposition; no graph decomposition is assumed.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_finite_double_curve_pieces line 15