OAI/Geometry/ProjectionBody/GraphProjection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ProjectionCounterexample.graphProjection_normDet line 14

   Source documentation

   Projection of a graph chart cancels the length of its unnormalized normal.

   theorem graphProjection_normDet {n : ℕ} (i : Fin (n + 1)) (a : E n)
       {u : E (n + 1)} (hu : ‖u‖ = 1) :
       ((project u).toLinearMap.comp (graphLinear i a)).normDet =
         |⟪graphNormal i a, u⟫| := by
   …

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

2. theorem OAI.ProjectionCounterexample.coordinateProjection_normDet line 33