OAI/Analysis/CircleDomains/Selection/SortedChordGapAvoidance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Enlarging the removed disks makes every closed retained gap avoid the original source disks, including at the new boundary endpoints.

  1. theorem OAI.CircleDomainRigidity.SortedCrossingChords.closed_gap_avoids_original line 15
  2. theorem OAI.CircleDomainRigidity.SortedCrossingChords.at_most_one_hole_for_disk line 30