OAI/Analysis/CircleDomains/Uniformization/ConformalInverse.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual inverse of an injective conformal sphere map

Local analytic inverse functions agree with the set-theoretic inverse on an open source domain. Thus an injective conformal map has a genuine two-sided conformal equivalence with its image.

  1. theorem OAI.CircleDomainRigidity.continuousAt_conformal_invFunOn line 20
  2. theorem OAI.CircleDomainRigidity.isConformalAt_invFunOn line 30
  3. theorem OAI.CircleDomainRigidity.isConformalEquivalence_of_injOn line 68