OAI/Geometry/SurfaceImmersion/Whitney/RegularPathCoverGerms.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An embedded finite regular path has genuine regular smooth arc germs outside a finite set of parameter values.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCover.region_eq_interval line 18
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.RegularPathCover.regular_germs_outside_finite line 25