OAI/Analysis/CircleDomains/Reflection/SphereClosedExteriorHomeomorph.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The normalized conformal map has an actual homeomorphism on the compact closed exterior. No boundary correspondence is assumed.

  1. lemma OAI.CircleDomainRigidity.exists_sphere_closed_exterior_homeomorph line 14