OAI/Geometry/SurfaceImmersion/Primitive/PhaseCurveCrossings.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic ordered crossing invariants for the fixed later curves. Their values can be computed in whichever phase chart is being corrected.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.crossing line 18
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.crossing_transition line 26