OAI/Geometry/SurfaceImmersion/Whitney/FiniteSingularProjection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

An actual smooth map of every compact surface into three-space with only finitely many singular points. The regularity of its direction parameter maps is retained for the subsequent local analysis.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.projectionJet line 20
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.projectionJet_smooth line 24
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.finite_singular_projection line 31
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.exists_finite_singular_projection line 83
  5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_smooth_three_map_finite_singular line 103