OAI/Geometry/SurfaceImmersion/Whitney/CompactDoublePairs.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The compactification of the double-pair locus can meet the diagonal only at singular points. Removing open crosscap neighborhoods leaves a compact set of genuine distinct double pairs.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.surfaceDoublePairs line 15
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.doublePairs_closure_diagonal_singular line 18
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.doublePairs_closure_equal line 28
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_doublePairs_exterior line 33