OAI/Geometry/SurfaceImmersion/Atlas/PhaseCovectorRead.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual covector in a tangent frame is the derivative of the scalar phase in that chart.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.covectorFrame_mfderiv line 17