OAI/Geometry/SurfaceImmersion/Atlas/SupportedChartEquiv.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Invertible local-chart transport on supported fields and their linear operators.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.chartPull_zero line 19
  2. def OAI.ClosedSurfaceR4.JetPolynomial.chartPull line 30
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.chartPull_apply line 39
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.chartPull_push line 44
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.chartPush_pull line 56
  6. def OAI.ClosedSurfaceR4.JetPolynomial.chartEquiv line 70
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.chartPull_bound line 81