OAI/Geometry/SurfaceImmersion/Whitney/EuclideanImmersionReduction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Dimension reduction of the ordinary Whitney embedding to a smooth immersion of a compact surface in four-dimensional Euclidean space.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.euclideanPad line 12
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.euclideanPad_injective line 20
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_immersion_postcompose line 31
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.reduce_immersion_dimension line 45
  5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_smooth_euclidean_four_immersion line 68

    Source documentation

    The ordinary four-dimensional immersion is proved without the three-dimensional Whitney input used in the conditional isometric theorem.

    theorem exists_smooth_euclidean_four_immersion :
    ∃ F : M → ProjectionTarget 4, ContMDiff planeModel 𝓘(ℝ,ProjectionTarget 4) ∞ F ∧
      ∀ p, Function.Injective (mfderiv planeModel 𝓘(ℝ,ProjectionTarget 4) F p) := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ProjectionTarget, OAI.ClosedSurfaceR4.planeModel