OAI/Geometry/SurfaceImmersion/Primitive/UniformConvexCircularAtlas.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A circular cover selected after local phase convexity has been fixed. All metric bounds are measured in the original, independent atlas.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circular_radius_le_of_subordinate line 16
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.uniform_convex_circular_atlas line 35