OAI/Geometry/SurfaceImmersion/Whitney/SurfaceDoublePairChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every transverse distinct double pair has an open real-line chart in the actual surface double-pair locus.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.surface_double_pair_chart line 17