OAI/Geometry/SurfaceImmersion/Whitney/FixedSurfacePairPatch.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Pair patches and their cutoffs are fixed before the surface map or perturbation size. Whole closed crosscap neighborhoods may be frozen.

  1. structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SurfacePairTranslationPatch line 16
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_fixed_surface_pair_patch line 31
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SurfacePairTranslationPatch.regularize line 66