OAI/Analysis/CircleDomains/Topology/FiniteJordanUniformization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One finite cycle makes every Jordan boundary analytic. Applying the proved invariant-coefficient construction then uniformizes the original finite Jordan exterior.

  1. lemma OAI.CircleDomainRigidity.exists_fin_jordan_uniformization line 15
  2. lemma OAI.CircleDomainRigidity.exists_finite_jordan_uniformization line 31