OAI/Geometry/SurfaceImmersion/Primitive/ReferenceCircularMargins.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compact positive inverse margins in the actual reference chart frames.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.chartCoefficient line 21
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.chartReference line 24
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.chartCoefficient_smoothOn line 27
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.chartReference_smooth line 33
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.chartCoefficient_positive line 36
  6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.inverse_margin line 45