OAI/Analysis/CircleDomains/Topology/PrincipalHomeomorphCompactness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A common exterior principal bound gives compactness of the maps and inverses directly. The limits keep the original principal scale.

  1. lemma OAI.CircleDomainRigidity.principal_smooth_homeomorph_subsequence line 14
  2. lemma OAI.CircleDomainRigidity.principal_limit_decay line 44