OAI/Geometry/SurfaceImmersion/Correction/InitialSmoothTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Start the finite smooth assembly at the original source endpoint, retaining its actual regular germ and an exact unchanged initial trace.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.initial_smooth_tail line 16
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.initial_smooth_tail_until line 29