OAI/Analysis/CircleDomains/Topology/ImageCoreBoundary.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Images of compact retained cores

A conformal injection on an open neighborhood carries a compact core's interior and boundary to the interior and boundary of its image. Regular closed cores remain regular closed. These facts use local openness, not a boundary extension of the conformal map.

  1. theorem OAI.CircleDomainRigidity.interior_image_of_continuous_open line 21
  2. theorem OAI.CircleDomainRigidity.interior_image_compact_core line 40
  3. theorem OAI.CircleDomainRigidity.frontier_image_of_continuous_open line 48
  4. theorem OAI.CircleDomainRigidity.frontier_image_compact_core line 59
  5. theorem OAI.CircleDomainRigidity.closure_image_interior_of_continuous line 67
  6. theorem OAI.CircleDomainRigidity.closure_image_core_interior line 78