OAI/Geometry/SurfaceImmersion/Atlas/AtlasMetricBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Smoothness and elementary norm operations for actual global metric tensors.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.inducedTensor_smooth line 28
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.linearMetricTensor_smooth line 38
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorWeightedBound_add line 50