OAI/Analysis/CircleDomains/Topology/ImageEndComponents.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual image-core chains for every complementary component

The source cores and their boundary parametrizations are constructed. Their images determine finite disjoint target Jordan families; every component of the complement of the conformal image is the strictly nested intersection of the selected target disks.

  1. theorem OAI.CircleDomainRigidity.exists_jordan_chain_for_complementary_component line 25