OAI/Analysis/CircleDomains/Selection/DenseComplementaryDust.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A totally disconnected subset of the sphere has empty interior. This supplies actual density of the component quotient domain in the countable selection.

  1. theorem OAI.CircleDomainRigidity.dense_compl_of_totallyDisconnected_sphere line 13