OAI/Geometry/SurfaceImmersion/Whitney/CornerBridgePath.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Turning a separated smooth corner bridge into an embedded replacement path, retaining finite regular pieces and the exact unchanged trace.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.leftPoint line 15
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.rightPoint line 17
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.source_eq line 20
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.target_eq line 26
  5. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.path line 32
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.path_injective line 35
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.path_range line 38
  8. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.initialPath line 41
  9. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.finalPath line 44
  10. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.replacement line 47
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.initialPath_range line 50
  12. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.finalPath_range line 62
  13. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.replacement_range line 74
  14. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge.replacement_finite_regular line 80