OAI/Geometry/SurfaceImmersion/Whitney/CleanSurfacePairs.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Regular pairs which additionally have no coincidence involving the prescribed finite singular set form an open, stable condition.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.cleanSurfacePairs line 16
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.mem_cleanSurfacePairs line 19
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.cleanSurfacePairs_open line 33
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_clean_pair_stability line 44