OAI/Geometry/SurfaceImmersion/Whitney/CrosscapKernelLine.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Explicit coordinates for the kernel line of a regular crosscap.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tangentRayCoefficient line 11
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tangentTransverseCoefficient line 13
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tangentRay_decomposition line 16
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel_eq_tangentRay_line line 22
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscap_kernel_line line 36