OAI/Geometry/ProjectionBody/ProductFacetProjection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ProjectionCounterexample.productFacetProjection_normDet line 12

   Source documentation

   The true projected area scale of each product facet chart.

   theorem productFacetProjection_normDet (i : Bool × Option (Fin 10))
       {u : E 20} (hu : ‖u‖ = 1) :
       ((project u).toLinearMap.comp (productFacetLinear i)).normDet =
         |productFunctional i u| := by
   …

   Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.project, OAI.ProjectionCounterexample.productFacetLinear, OAI.ProjectionCounterexample.productFunctional