OAI/Analysis/CircleDomains/Topology/CompactClopenRefinement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite clopen partitions subordinate to prescribed dust neighborhoods

This retains the compact pieces and their containment data, rather than only the open cover returned by DustCover. They are the pieces pulled back to the physical sphere before simultaneous smooth contour construction.

  1. theorem OAI.CircleDomainRigidity.exists_compact_clopen_refinement line 17