OAI/Analysis/CircleDomains/Topology/JordanSideCorrespondence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Correspondence of the source and image sides of a core boundary

Connectivity of the source on a disk's inside, together with local openness at its retained boundary, determines which target Jordan disk it maps into. This tracks the labels of boundary curves without extending the conformal map across any omitted component.

  1. theorem OAI.CircleDomainRigidity.isPreconnected_sphere_jordan_intersection line 25
  2. theorem OAI.CircleDomainRigidity.open_image_jordan_side_subset line 39
  3. theorem OAI.CircleDomainRigidity.conformal_image_jordan_side_subset line 128
  4. theorem OAI.CircleDomainRigidity.open_image_jordan_side_eq line 144
  5. theorem OAI.CircleDomainRigidity.conformal_image_jordan_side_eq line 178