OAI/Analysis/CircleDomains/Topology/HolomorphicHomeomorph.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A holomorphic plane homeomorphism has a holomorphic inverse on the image domain. Isolated critical points are removed from the continuous inverse; the chain rule then excludes them altogether.

  1. theorem OAI.CircleDomainRigidity.holomorphicHomeomorph_deriv_not_locally_zero line 16
  2. theorem OAI.CircleDomainRigidity.holomorphicHomeomorph_inverse_differentiableAt line 36
  3. theorem OAI.CircleDomainRigidity.holomorphicHomeomorph_deriv_ne_zero line 60
  4. theorem OAI.CircleDomainRigidity.holomorphicHomeomorph_conformal line 73