OAI/Geometry/SurfaceImmersion/Whitney/SmoothSurfaceDoubleChart.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The real-line charts of the actual double locus have smooth regular inverses.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_surface_double_pair_chart_data line 17
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_surface_double_pair_chart line 121