OAI/Geometry/SurfaceImmersion/Primitive/CrossingChoiceScaling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Crossing normal choices are invariant under the positive squares arising when a nonvertical curve direction is written in slope coordinates.

  1. lemma OAI.ClosedSurfaceR4.GeometryPreservation.crossing_choice_scale line 12
  2. lemma OAI.ClosedSurfaceR4.GeometryPreservation.realSecondForm_smul_self line 27
  3. lemma OAI.ClosedSurfaceR4.GeometryPreservation.realSecondForm_firstSlope line 33
  4. lemma OAI.ClosedSurfaceR4.GeometryPreservation.crossing_choice_firstSlope line 43