FiniteExitArcAt.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Identify exit arcs from any strictly positive local departure time. This permits a short initial departure inside a marked corner chart.

theorem OAI.SLEExactGauge.RibbonCoordinates.finite_exit_event_measure_le_arc_at line 15