OAI/Geometry/SurfaceImmersion/Primitive/CircularPhaseDefiningFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite exceptional tangencies of actual coordinate circles supply all local defining functions required by the supported angular loop.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circular_phase_defining_family line 17