OAI/Analysis/CircleDomains/Topology/ThickenedContinuumDisk.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A small open neighborhood of a connected subset of the closed disk remains connected when restricted to the open disk.

  1. lemma OAI.CircleDomainRigidity.exists_inner_disk_scale line 13
  2. lemma OAI.CircleDomainRigidity.inner_disk_scale_dist line 19
  3. lemma OAI.CircleDomainRigidity.isConnected_thickening_inter_disk line 28