OAI/Geometry/SurfaceImmersion/Atlas/AtlasUniformNorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform value and first-jet consequences of the fixed atlas norms.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.weightedBound_uniform_norm line 16
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.weightedBound_C1 line 36
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.weighted_immersion_tolerance line 45