OAI/Analysis/CircleDomains/Uniformization/JordanCircularizationStep.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One exact Koebe circularization step on a finite family of disjoint Jordan holes. The selected hole becomes round, all other holes are the actual conformal images, and the entire exterior is carried bijectively onto the new exterior.

  1. lemma OAI.CircleDomainRigidity.exists_jordan_circularization_step_full line 17
  2. lemma OAI.CircleDomainRigidity.exists_jordan_circularization_step line 119