OAI/Geometry/SurfaceImmersion/Atlas/ReferenceCoordinateData.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Size, identity and positivity of the fixed reference data in any active chart. The constants precede every independent radius and phase choice.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.coordinateReference line 29
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.coordinateReference_identity line 34
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.coordinateReference_coefficient line 51
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ReferenceCircularAtlas.coordinateReference_bound line 64