OAI/Geometry/SurfaceImmersion/Atlas/AtlasImmersionGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local good-phase geometry in any covering chart gives the intrinsic immersion and nonzero second-form hypotheses for the next primitive.

  1. lemma OAI.ClosedSurfaceR4.coordinateMap_injective_of_immersion line 18
  2. lemma OAI.ClosedSurfaceR4.nonzero_secondForm_of_chart_good line 35
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.immersion_of_planeRead_injective line 82
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.geometry_of_chartwise_good line 102