OAI/Geometry/SurfaceImmersion/Primitive/TransverseCircularRadii.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Generic radii give transverse actual coordinate circles, not merely regular levels of their auxiliary global extensions.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.exists_transverse_circular_radii line 19
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCrossingSet line 49
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCrossingSet_finite line 54