OAI/Geometry/SurfaceImmersion/Whitney/CrosscapLinearStability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A uniform local injectivity estimate for a nondegenerate direction map. It will allow the quadratic jet to replace the original map near a crosscap.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.near_equiv_derivative_injOn line 14
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.local_linearization_stability_on line 42
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.local_linearization_stability line 76