OAI/Geometry/SurfaceImmersion/Primitive/PreparedPhaseCrossingSlopes.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The generic phase selection makes each relevant transported boundary direction nonvertical, and a finite crossing set has a fixed slope bound.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PhaseBoundaryCurve.directionIn_first_ne_of_covectors line 19
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finite_crossing_slope_bound line 35