OAI/Analysis/CircleDomains/Selection/FiniteAnalyticRounding.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous smooth rounding of a finite disjoint analytic Jordan family. The actual ambient diffeomorphism fixes the complement of a bounded disk.

  1. lemma OAI.CircleDomainRigidity.exists_finite_analytic_rounding line 16