OAI/Geometry/SurfaceImmersion/Primitive/CircularRadiusCovectors.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The smooth radius fields used for Sard have exactly the true circle normal covectors on the new boundaries. Their regular pairs are transverse.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularNormalCovector line 15
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circularRadiusField_covector line 22
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.actual_circular_normals_independent line 40