OAI/Analysis/CircleDomains/Uniformization/JordanExteriorDiskChart.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite simply connected chart of a Jordan-hole exterior. It is normalized at the original point at infinity, which has chart value zero.

  1. lemma OAI.CircleDomainRigidity.isSimplyConnected_sphere_jordan_exterior line 15
  2. lemma OAI.CircleDomainRigidity.finite_chart_simplyConnected line 35
  3. lemma OAI.CircleDomainRigidity.finite_chart_proper_of_complement_nontrivial line 45
  4. def OAI.CircleDomainRigidity.jordanExteriorPlane line 57
  5. lemma OAI.CircleDomainRigidity.jordan_exterior_plane_data line 61