OAI/Geometry/SurfaceImmersion/Whitney/AdaptedDoubleSheetModels.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Constructed smooth models of the two actual sheets, using the same parameter on their common curve.

  1. structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalDoubleSheetModel line 18
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothDoubleChart.adapted_sheet_models line 42
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalDoubleSheetModel.crossing_regular line 95