OAI/Geometry/SurfaceImmersion/Correction/AtlasMetricLocalModel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local coordinate models of the complete perturbed global metric.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorChartRead_add line 34
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.metric_read_on_support line 39
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_metric_local_model line 49