OAI/Geometry/SurfaceImmersion/Primitive/FiniteCircularPreparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The geometric finite preparation: independent radii and linear phase parts are chosen before the starting immersion is flattened at the finite crossing set. All statements concern the actual coordinate circles.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.finite_circular_preparation line 20