OAI/Analysis/SphereIsometry/AlignmentSet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual closed convex invariant subset of the extremal sphere

The generic positive scheduling theorem is instantiated with the proved common-support hull growth. No convexity of the full extremal set is assumed.

  1. theorem OAI.Tingley.exists_return_invariant_convex line 21