OAI/Geometry/SurfaceImmersion/Primitive/CrossingPositivePairing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The boundary Gauss inequality used when matching the interior and exterior preferred normals.

  1. lemma OAI.ClosedSurfaceR4.VelocityFrame.dot_square_le_self_of_unit line 13
  2. lemma OAI.ClosedSurfaceR4.VelocityFrame.secondForm_gauss_directions line 21
  3. lemma OAI.ClosedSurfaceR4.VelocityFrame.orderedCrossing_le_pure_pairing line 38
  4. lemma OAI.ClosedSurfaceR4.VelocityFrame.orderedCrossing_pos_pure_pairing line 57