OAI/Geometry/SurfaceImmersion/Whitney/SmoothCrosscapAxisTangent.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual smoothed source arc has a nonzero axial velocity and zero image velocity at its singular endpoint.

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