OAI/Geometry/SurfaceImmersion/Whitney/DoubleArcChartPartition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A compact embedded arc in the actual transverse double locus has a finite ordered subdivision into the smooth regular chart arcs constructed above.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.double_arc_chart_partition line 17
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finite_smooth_double_arc_pieces line 45