OAI/Analysis/CircleDomains/Selection/SortedCrossingChords.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Sorting the actual crossed disks gives a finite ordered hole family with an injective owner map and exact signed flux accounting.

  1. theorem OAI.CircleDomainRigidity.horizontalChord_injective_on_crossing line 12
  2. structure OAI.CircleDomainRigidity.SortedCrossingChords line 25
  3. theorem OAI.CircleDomainRigidity.exists_sorted_crossing_chords line 37
  4. theorem OAI.CircleDomainRigidity.SortedCrossingChords.sum_hole_increments line 68
  5. theorem OAI.CircleDomainRigidity.SortedCrossingChords.monotone_first line 82
  6. theorem OAI.CircleDomainRigidity.SortedCrossingChords.monotone_last line 88