OAI/Geometry/SurfaceImmersion/Atlas/PhaseChartTransition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The localized analytic maps have the same second forms as the actual surface phase charts. This permits later curves to keep their own charts.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseRealChartMap_surface_germ line 19
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseRealChartMap_transition_germ line 34
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_secondForm_transition line 56
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_intrinsic_crossing_transition line 90