OAI/Analysis/CircleDomains/Topology/PrescribedJordanCore.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite smooth Jordan core retaining a prescribed connected set

Sard, compact one-manifold classification and Schoenflies produce disjoint smooth filled contours around the complement. Their common exterior stays in the original domain and retains the prescribed compact set in its interior.

  1. theorem OAI.CircleDomainRigidity.exists_prescribed_jordan_core line 23