OAI/Geometry/ProjectionBody/GraphJacobian.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ProjectionCounterexample.graphLinear_normDet line 13

   Source documentation

   The Jacobian of a graph chart is the length of its unnormalized normal.

   theorem graphLinear_normDet {n : ℕ} (i : Fin (n + 1)) (a : E n) :
       (graphLinear i a).normDet = ‖graphNormal i a‖ := by
   …

   Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.graphLinear, OAI.ProjectionCounterexample.graphNormal