OAI/Geometry/Immersion/ClosedSurface/AtlasPhases.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClosedSurfaceR4.phaseLinear line 15
  2. lemma OAI.ClosedSurfaceR4.phaseLinear_apply line 18
  3. def OAI.ClosedSurfaceR4.atlasPhase line 20
  4. lemma OAI.ClosedSurfaceR4.atlasPhase_smoothOn line 22
  5. def OAI.ClosedSurfaceR4.phaseDerivative line 27
  6. lemma OAI.ClosedSurfaceR4.phaseDerivative_linear_comp line 30
  7. theorem OAI.ClosedSurfaceR4.actual_phase_differential line 40
  8. lemma OAI.ClosedSurfaceR4.coordinateTransition_apply_chart line 50
  9. lemma OAI.ClosedSurfaceR4.coordinateTransition_mem_chart line 57
  10. def OAI.ClosedSurfaceR4.atlasPhaseCovector line 67
  11. theorem OAI.ClosedSurfaceR4.actual_phase_margin_at line 70