OAI/Analysis/CircleDomains/Uniformization/RecursiveLimitDust.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every complementary component of the actual recursive conformal limit is a point. Matched ends and the saved finite-stage barriers supply all geometric and energy data.

  1. theorem OAI.CircleDomainRigidity.AppendingSequence.recursive_limit_component_singleton line 23
  2. theorem OAI.CircleDomainRigidity.AppendingSequence.recursive_limit_complement_totallyDisconnected line 84