OAI/Analysis/CircleDomains/Topology/ImageCoreJordan.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual Jordan disks bounded by an image core

Schoenflies is applied only to the images of the given boundary circles. The image-core theorem then proves that their filled sides are pairwise disjoint and exhaust the complement of the image core.

  1. theorem OAI.CircleDomainRigidity.continuousAt_finite_part_of_conformalAt line 22
  2. theorem OAI.CircleDomainRigidity.exists_jordan_image_core_of_continuous_open line 34
  3. theorem OAI.CircleDomainRigidity.exists_jordan_image_core line 117