OAI/Geometry/SurfaceImmersion/Atlas/RealPhaseChart.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual phase chart in the real pair coordinates used by curvature.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.realPhaseChart line 11
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.realPhaseChart_apply line 16
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.realPhaseChart_symm_apply line 19
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.realPhaseChart_source line 22
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.realPhaseChart_target line 25
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.realPhaseChart_smooth line 28
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.realPhaseChart_symm_smooth line 32