OAI/Analysis/CircleDomains/Selection/DustCover.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Small disjoint neighborhoods of compact dust

A compact totally disconnected subset of a metric space admits finite open covers with pairwise disjoint closures of arbitrarily small diameter.

  1. theorem OAI.CircleDomainRigidity.exists_small_disjoint_open_cover_of_compact_dust line 18