OAI/Geometry/SurfaceImmersion/Primitive/PreparedCircularDefiners.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Generic circle crossings and phase tangencies give exactly the finite exception set used by the supported angular-loop construction.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.prepared_circular_definers line 17