OAI/Geometry/SurfaceImmersion/Whitney/CrosscapKernelCapture.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A kernel near a crosscap is captured in the same affine direction chart, with an explicit bound on its direction parameter.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tangentRay_sub line 13
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_fixed_tangentRay_kernel line 17
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_near_tangentRay_kernel line 68
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel_capture_near line 83
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscap_transverse_derivative_ne_zero line 110