OAI/Analysis/CircleDomains/Topology/CyclicBoundaryCorrespondence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact boundary correspondences for the actual one-hole maps used by the finite circularization iteration.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.Step.closed_exterior_correspondence line 18
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.cyclic_closed_exterior_correspondence line 26