OAI/Analysis/CircleDomains/Uniformization/JordanConfigurationExterior.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The fixed finite source configuration has a common exterior disk and a connected finite chart. These provide the domains for normal families.

  1. def OAI.CircleDomainRigidity.FiniteJordanConfiguration.planeRegion line 13
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.planeRegion_eq line 17
  3. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.planeRegion_open line 24
  4. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.exists_exterior_radius line 27
  5. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.planeRegion_connected line 38