OAI/Geometry/SurfaceImmersion/Whitney/SharedParameterArcJoin.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual arc joining through two forward smooth germs of the same underlying path parameter.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.join_shared_parameter_arcs line 14