OAI/Analysis/CircleDomains/Topology/JordanDiskCompression.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact subsets of a Jordan disk can be shrunk by an ambient homeomorphism which fixes the whole exterior of that disk.

  1. lemma OAI.CircleDomainRigidity.exists_compression_in_jordan_disk line 13
  2. lemma OAI.CircleDomainRigidity.exists_small_supported_continuum_compression line 48