OAI/Analysis/CircleDomains/Sobolev/SmoothRealSphereMaps.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Smooth finite charts of sphere equivalences fixing infinity

The two genuine inverses induce smooth inverse maps in finite real coordinates. Their restriction to any open source region is open, which supplies the domain of each transported masked coordinate.

  1. theorem OAI.CircleDomainRigidity.IsSmoothSphereAt.contDiffAt_sphereRealMap line 24
  2. theorem OAI.CircleDomainRigidity.coe_finiteCoord line 41
  3. theorem OAI.CircleDomainRigidity.sphereRealMap_mem line 44
  4. theorem OAI.CircleDomainRigidity.sphereRealMap_left_inverse line 53
  5. theorem OAI.CircleDomainRigidity.isOpen_realChartDomain line 63
  6. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.inverse_fixes_infty line 74
  7. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.infty_mem_target line 77
  8. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.finite_inv line 79
  9. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.finite_forward line 83
  10. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.real_bijOn line 86
  11. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.real_left_inv line 95
  12. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.real_right_inv line 99
  13. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.real_smooth line 103
  14. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.real_smooth_inv line 107
  15. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.real_image_eq line 111
  16. theorem OAI.CircleDomainRigidity.IsSmoothSphereEquivalence.isOpen_real_image line 122