OAI/Geometry/SurfaceImmersion/Whitney/SmoothFiniteRegularPath.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite embedded regular-piece path can be smoothed inside any open set containing its interior. All new points lie in a compact subset of that open set, while its two endpoints remain fixed.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_finite_regular_path line 16