OAI/Geometry/SurfaceImmersion/Atlas/TensorPhaseDifferential.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Restored rank-one tensor coordinates are the actual differentials of atlas phases.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorComponent_apply line 29
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorComponent_tangentCoordinates line 43
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorRestore_apply line 55
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.coordinateChart_tangentCoordinates line 70
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorRestore_covectorSquare line 87