OAI/Analysis/CircleDomains/Uniformization/AnalyticCapRounding.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Round one analytic Jordan cap by an actual compactly supported smooth plane diffeomorphism inside any prescribed open neighborhood.

  1. lemma OAI.CircleDomainRigidity.exists_smooth_analytic_cap_rounding line 14