OAI/Geometry/SurfaceImmersion/Primitive/IntrinsicCrossingNaturality.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The intrinsic ordered crossing is expressed entirely by the second fundamental form, and is unchanged under smooth coordinate changes.

  1. lemma OAI.ClosedSurfaceR4.VelocityFrame.orderedCrossing_intrinsic_eq line 16
  2. lemma OAI.ClosedSurfaceR4.VelocityFrame.orderedCrossing_intrinsic_eq_on line 32
  3. lemma OAI.ClosedSurfaceR4.VelocityFrame.orderedCrossing_intrinsic_comp line 53
  4. lemma OAI.ClosedSurfaceR4.VelocityFrame.orderedCrossing_intrinsic_germ line 72
  5. lemma OAI.ClosedSurfaceR4.VelocityFrame.orderedCrossing_intrinsic_comp_on line 84