OAI/Geometry/SurfaceImmersion/Atlas/JetPhaseChartFromReal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The whole-disk real phase charts in the coordinate representation used by the nonlinear primitive construction.

  1. def OAI.ClosedSurfaceR4.jetPhaseChart line 14
  2. lemma OAI.ClosedSurfaceR4.jetPhaseChart_apply line 18
  3. lemma OAI.ClosedSurfaceR4.jetPhaseChart_symm_apply line 21
  4. lemma OAI.ClosedSurfaceR4.jetPhaseChart_source line 24
  5. lemma OAI.ClosedSurfaceR4.jetPhaseChart_smooth line 27
  6. lemma OAI.ClosedSurfaceR4.jetPhaseChart_symm_smooth line 31
  7. lemma OAI.ClosedSurfaceR4.surfacePhaseChart_jetPhaseChart_apply line 37
  8. lemma OAI.ClosedSurfaceR4.surfacePhaseChart_jetPhaseChart_source line 42