OAI/Analysis/CircleDomains/Topology/PlaneHomeomorphFromSphere.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Restrict an actual sphere homeomorphism fixing infinity to its finite plane chart.

  1. def OAI.CircleDomainRigidity.spherePlaneMap line 13
  2. lemma OAI.CircleDomainRigidity.spherePlaneMap_finite line 16
  3. lemma OAI.CircleDomainRigidity.coe_spherePlaneMap line 21
  4. lemma OAI.CircleDomainRigidity.spherePlaneMap_continuous line 25
  5. lemma OAI.CircleDomainRigidity.sphereHomeomorph_symm_infty line 32
  6. def OAI.CircleDomainRigidity.spherePlaneHomeomorph line 37