OAI/Geometry/SurfaceImmersion/Whitney/DoubleLocusSmoothStructure.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The transverse ordered double locus carries its actual smooth one-dimensional manifold structure, built from the proved submersion charts.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.transverseDoubleChart line 15
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.transverseDoubleChart_mem line 21
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.doubleLocusChartedSpace line 28
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.doubleLocus_isManifold line 37