OAI/Analysis/CircleDomains/Rigidity/MatchedImageCores.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Matched source and target Jordan cores

The actual mapped boundary parametrizations identify each target disk's label. Both inclusions of the corresponding source/target side equality are proved, so refinement can carry those labels to end components.

  1. theorem OAI.CircleDomainRigidity.exists_matched_image_core_of_continuous_open line 23
  2. theorem OAI.CircleDomainRigidity.exists_matched_image_core line 69
  3. theorem OAI.CircleDomainRigidity.exists_matched_jordan_exhaustion_of_continuous_open line 86
  4. theorem OAI.CircleDomainRigidity.exists_matched_jordan_exhaustion line 107