OAI/Geometry/SurfaceImmersion/Whitney/CrosscapDoubleRay.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The image of the local double curve is an actual regular half-ray. Its acceleration is forced to be nonzero by the regular direction jet.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscap_kernel_acceleration_ne_zero line 13
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.centeredSurfaceTaylor_value line 27
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscap_kernel_image line 38
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscap_double_ray_injective line 50