OAI/Analysis/CircleDomains/Reflection/SphereClosedExteriorCoordinates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The spherical and planar closed-exterior extensions are the same at every finite point. The spherical image is the entire closed disk.

  1. lemma OAI.CircleDomainRigidity.coe_mem_closed_jordan_exterior line 13
  2. lemma OAI.CircleDomainRigidity.sphere_plane_closed_exterior_eq line 19
  3. lemma OAI.CircleDomainRigidity.analytic_sphere_closed_exterior_image line 64