OAI/Analysis/CircleDomains/Rigidity/EnclosedCircleChords.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Chords of disks inside an outer circle. The selected crossed disks are exactly those whose transverse interval contains the line.

  1. theorem OAI.CircleDomainRigidity.horizontalChord_strict line 13
  2. theorem OAI.CircleDomainRigidity.horizontalChord_endpoint_dist line 23
  3. theorem OAI.CircleDomainRigidity.axialChord_endpoint_dist line 35
  4. theorem OAI.CircleDomainRigidity.enclosed_crossing_iff line 42