FiniteDustCover.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite disjoint smooth covers of relatively clopen dust

Connected-complement sphere neighborhoods inside a prescribed open set admit subordinate compact clopen dust pieces. Simultaneous physical contours give disjoint closed fills avoiding the entire physical complement.

theorem OAI.CircleDomainRigidity.exists_finite_smooth_physical_dust_cover line 20