OAI/Analysis/SphereIsometry/IteratedSubdivision.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Actual subdivisions used in the geometric Sperner argument
The finite recursion satisfies incidence, boundary restriction, zero-dimensional counting, coordinate support, and shrinking mesh properties. These yield the geometric Sperner and simplex fixed-point theorems without additional triangulation or incidence assumptions.
This file declares nothing itself. It gathers the 6 imports below, so a file that imports it gets all of them.