OAI/Geometry/SurfaceImmersion/Atlas/OuterPhaseGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The fixed outer plateau, including points outside the partition weight, retains the actual immersion, metric and normal in phase coordinates.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseRealChartMap_surface_germ_of_outer line 18
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.realChartMap_germ_of_outer line 31
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.realChartMap_metric_germ_of_outer line 49
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.realChartMap_injective_of_outer line 64
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.preferred_normal_in_phase_of_outer line 74