OAI/Analysis/CircleDomains/Topology/JordanCoreRecognition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Recognizing the exterior bounded by a finite Jordan family

A regular closed sphere set with connected interior containing infinity and with finitely many disjoint Jordan boundary curves is exactly their common closed exterior. The filled disks are disjoint. This supplies the image-side identification of retained cores without assuming orientation or a boundary extension theorem.

  1. theorem OAI.CircleDomainRigidity.unbounded_preconnected_subset_jordan_exterior line 23
  2. theorem OAI.CircleDomainRigidity.sphere_jordan_core_recognition line 43