CrosscutSeparationInput.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The unit-disk specialization of the classical crosscut separation theorem. Published statement: M. D. Contreras and S. Díaz-Madrigal, Fractional iteration in the disk algebra: prime ends and composition operators, Rev. Mat. Iberoamericana 21 (2005), 911–928, §3, p. 918, first paragraph defining crosscuts: the complement has two connected components and each component's boundary inside the domain is the crosscut. https://ems.press/content/serial-article-files/38137

def OAI.CircleDomainRigidity.UnitDiskCrosscutSeparation line 22
Source documentation
Exactly two open connected components, with the stated relative frontier. The endpoints belong to the circle and the open arc belongs to the disk.
```
def UnitDiskCrosscutSeparation : Prop :=
…
```