OAI/Geometry/SurfaceImmersion/Primitive/TwoMechanismCrossing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The turn threshold is fixed before any bound on the loop's transverse coefficient. The longitudinal threshold is allowed to depend on that bound.

  1. theorem OAI.ClosedSurfaceR4.GeometryPreservation.longitudinal_ordered_crossing_threshold line 11
  2. theorem OAI.ClosedSurfaceR4.GeometryPreservation.two_mechanism_crossing_threshold line 29