OAI/Analysis/CircleDomains/Uniformization/ConformalLocalInverse.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local inverses in sphere charts

On an open set the chart expressions of a conformal sphere map are analytic. The ordinary complex inverse function theorem therefore identifies its neighborhood filters. An injective conformal map then has a conformal inverse on its image, with no global extension assumed.

  1. theorem OAI.CircleDomainRigidity.IsConformalOn.analyticAt_sphereLocalMap line 21
  2. theorem OAI.CircleDomainRigidity.map_chartSymm_nhds line 49
  3. theorem OAI.CircleDomainRigidity.IsConformalOn.map_nhds_eq line 59
  4. theorem OAI.CircleDomainRigidity.IsConformalOn.isOpen_image line 86