OAI/Geometry/SurfaceImmersion/Whitney/CompactArcLastIntersection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The last intersection of a compact curve with a closed set leaves a terminal arc disjoint from that set. No finiteness of intersections is assumed.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_curve_last_intersection line 14
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_arc_last_intersection line 33