OAI/Analysis/CircleDomains/Uniformization/AnalyticCapShrink.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Shrink one actual analytic Jordan cap within any prescribed open neighborhood. The ambient map and its inverse are smooth and fix every point outside one compact subset of that neighborhood.

  1. lemma OAI.CircleDomainRigidity.exists_analytic_cap_shrinker line 18