OAI/Analysis/CircleDomains/Topology/BoundaryArcComplement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The unused part of the unit circle after closing a crosscut is one connected open arc, with its exact angular parameter interval.

  1. lemma OAI.CircleDomainRigidity.boundaryClosingArc_complement_image line 13
  2. lemma OAI.CircleDomainRigidity.isConnected_boundaryClosingArc_complement line 50