OAI/Geometry/SurfaceImmersion/Correction/CorrectionGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The fixed atlas data used when taking the smooth correction limit.

  1. structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CorrectionGeometry line 33
  2. abbrev OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.toCorrectionGeometry line 40
  3. instance OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.(instance at line 44) line 44