OAI/Geometry/SurfaceImmersion/Atlas/MetricAtlasReference.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual smooth metric section gives the reference tensor used by the compact good-phase construction.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.metric_inner_smooth line 37
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorComponent_metric line 44
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorPlaneRead_metric_on_weight line 74
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorPlaneRead_metric line 88
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorPlaneRead_metric_smooth line 95