OAI/Analysis/CircleDomains/Selection/TranslatedRayOrder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The side of one translated ray relative to another is fixed by their starting order on the real boundary.

  1. theorem OAI.CircleDomainRigidity.translated_curve_avoids_crosscut line 15
  2. theorem OAI.CircleDomainRigidity.translated_ray_side_value line 34
  3. theorem OAI.CircleDomainRigidity.later_ray_right line 72
  4. theorem OAI.CircleDomainRigidity.earlier_ray_left line 82