OAI/Geometry/SurfaceImmersion/Whitney/QuadraticCrosscapIsolation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The prepared quadratic model has a single singularity in a fixed neighborhood. Its two local sheets meet exactly along the kernel line.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.centeredSurfaceTaylor_isolated_crosscap line 14
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.centeredSurfaceTaylor_reflected_difference line 30
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.centeredSurfaceTaylor_reflected_eq_iff line 40
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.quadratic_crosscap_double_points line 47