OAI/Geometry/SurfaceImmersion/Whitney/CornerGraphSeparation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Embeddedness forces strict separation of the two returning graph branches.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCornerChart.left_graph_realized line 15
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCornerChart.right_graph_realized line 24
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCornerChart.branch_graphs_ne line 33
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCornerChart.graphs_ne_on_overlap line 49
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCornerChart.graphs_ordered_on_interval line 58