OAI/Geometry/SurfaceImmersion/Atlas/AtlasFiniteCancellation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual finite global metric-linear corrections assembled from local phase solvers.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.jetChartMap line 30
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.jetChartMap_smooth line 33
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.jetChartMap_plane line 38
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_finite_cancellation line 41