OAI/Analysis/CircleDomains/Topology/DiskCrossingInput.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Pascoletti and Zanolin, A Crossing Lemma for Annular Regions and Invariant Sets with an Application to Planar Dynamical Systems, Journal of Mathematics (2013), Article 267393, DOI 10.1155/2013/267393, Lemma 7 and Remark 6, p. 3. In the closed unit disk, two compact connected sets containing four cyclically alternating boundary points intersect. The rational cut coordinate records that cyclic order.

  1. def OAI.CircleDomainRigidity.standardCirclePoint line 20
  2. theorem OAI.CircleDomainRigidity.standardCirclePoint_injective line 23
  3. def OAI.CircleDomainRigidity.UnitDiskAlternatingContinua line 26