OAI/Geometry/SurfaceImmersion/Whitney/OrderedArcEndpointUnique.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Singleton fibers over crosscaps prevent the source projection of an ordered connecting arc from revisiting either singular endpoint.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ordered_arc_endpoints_distinct line 12
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ordered_arc_source_start_unique line 19