OAI/Analysis/CircleDomains/Uniformization/FiniteCoreCorrespondence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Each actual circularization step extends to a homeomorphism of the entire compact finite core. The construction is restricted from the proved closed-exterior extension.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.Step.exists_core_correspondence_exact line 18
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.Step.exists_core_correspondence line 54