OAI/Analysis/CircleDomains/Topology/SphereLocalMapInjective.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

An analytic local chart of a sphere homeomorphism has nonzero complex derivative, obtained from genuine local injectivity.

  1. def OAI.CircleDomainRigidity.sphereLocalMapRegion line 13
  2. lemma OAI.CircleDomainRigidity.isOpen_sphereLocalMapRegion line 16
  3. lemma OAI.CircleDomainRigidity.center_mem_sphereLocalMapRegion line 21
  4. lemma OAI.CircleDomainRigidity.sphereLocalMap_injOn line 27
  5. lemma OAI.CircleDomainRigidity.sphereLocalMap_deriv_ne_zero line 39