OAI/Analysis/CircleDomains/Topology/DiskRemainder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Dust remaining after a finite contour family

When the physical boundaries miss the dust, removing the interiors of a finite family leaves compact relatively clopen dust disjoint from every closed fill. This supplies the invariant for the descending grid stages.

  1. theorem OAI.CircleDomainRigidity.quotient_cover_of_physical_cover line 18
  2. theorem OAI.CircleDomainRigidity.dust_inter_closed_fills_eq_inter_interiors line 31
  3. theorem OAI.CircleDomainRigidity.compact_clopen_dust_remainder line 49
  4. theorem OAI.CircleDomainRigidity.remainder_avoids_covered_set line 85