OAI/Analysis/CircleDomains/Selection/CrossingChords.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The holes actually crossed by a segment

Only disks meeting the segment are retained. Their horizontal chords lie strictly between its domain endpoints, are disjoint, and remove exactly the same points of the segment as the full family of disks.

  1. def OAI.CircleDomainRigidity.crossingDisks line 18
  2. def OAI.CircleDomainRigidity.crossingChords line 23
  3. theorem OAI.CircleDomainRigidity.mem_crossingDisks line 28
  4. theorem OAI.CircleDomainRigidity.crossingDisk_line_hit line 35
  5. theorem OAI.CircleDomainRigidity.crossingChords_inside line 42
  6. theorem OAI.CircleDomainRigidity.crossingChords_disjoint line 56
  7. theorem OAI.CircleDomainRigidity.crossingChords_domain line 68