OAI/Geometry/SurfaceImmersion/Atlas/AtlasBackgroundLowerBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The fixed coordinate lower bound dominates any fixed smooth background metric. Both constants are chosen before the finite preparation set.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.coordinateChart_differential line 21
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.uniform_background_metric_lower_bound line 40