OAI/Analysis/CircleDomains/Topology/ExteriorJordanCore.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A holomorphic principal exterior injection maps each closed exterior core to the closed exterior of its image Jordan curve. Schoenflies identifies the filled Jordan disk.

  1. lemma OAI.CircleDomainRigidity.exterior_closed_core_jordan line 18