OAI/Analysis/CircleDomains/Uniformization/FiniteJordanImageUniformization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite Jordan uniformization also applies after an arbitrary sphere homeomorphism. A conformal normalization makes its image of infinity the point at infinity, leaving an actual plane homeomorphism of all caps.

  1. lemma OAI.CircleDomainRigidity.spherePlaneHomeomorph_onePointCongr line 15
  2. lemma OAI.CircleDomainRigidity.trans_closed_jordan_image line 23
  3. lemma OAI.CircleDomainRigidity.exists_finite_jordan_image_uniformization line 28
  4. lemma OAI.CircleDomainRigidity.uniformize_constructed_finite_completion_after_homeomorphism line 63