OAI/Geometry/SurfaceImmersion/Whitney/CrosscapEndpointParameter.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A whole initial segment of the chosen embedded double arc is traced by the explicit pair of opposite kernel-axis curves, in one orientation.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscap_endpoint_parameter line 17