OAI/Geometry/SurfaceImmersion/Whitney/QuadraticDoublePoints.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Double points of a quadratic crosscap have a singular midpoint. In a neighborhood with one singular point their two preimages are reflections through that point.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.surfaceTaylorTwo_midpoint_identity line 14
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.centeredSurfaceTaylor_midpoint_identity line 26
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.centeredSurfaceTaylor_double_midpoint_singular line 38
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.centeredSurfaceTaylor_double_reflection line 48