OAI/Analysis/CircleDomains/Sobolev/HolomorphicInjOnDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The local inverse of a holomorphic injection on an open plane set. The inverse is first continuous by open mapping; isolated possible critical values are removable. Thus its actual derivative is nonzero.

  1. lemma OAI.CircleDomainRigidity.injOn_not_eventually_constant line 14
  2. lemma OAI.CircleDomainRigidity.holomorphicInjOn_map_nhds line 26
  3. lemma OAI.CircleDomainRigidity.continuousAt_holomorphic_invFunOn line 34
  4. lemma OAI.CircleDomainRigidity.holomorphicInjOn_deriv_not_eventually_zero line 44
  5. lemma OAI.CircleDomainRigidity.holomorphicInjOn_inverse_differentiableAt line 58
  6. lemma OAI.CircleDomainRigidity.holomorphicInjOn_deriv_ne_zero line 102