OAI/Geometry/SurfaceImmersion/Whitney/LocalCornerBridge.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Every actual corner of the finite embedded source path admits a small regular embedded bridge with oriented smooth attachment germs.

  1. structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.LocalCornerBridge line 18
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCornerChart.returning_bridge line 41
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCornerChart.advancing_bridge line 71
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.local_corner_bridge line 103