OAI/Analysis/CircleDomains/Selection/DisjointDustContours.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous contours for finitely many clopen dust pieces

Disjoint compact physical pieces have disjoint open neighborhoods. Regular contours and the outer subfamily of their combined family have disjoint closed fills inside the prescribed connected-complement containers.

  1. theorem OAI.CircleDomainRigidity.exists_disjoint_dust_contours line 19