OAI/Analysis/CircleDomains/Selection/TranslatedSideNesting.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The right components of integer translates form a decreasing family. This is derived from crosscut separation and the order of the actual starts.

  1. theorem OAI.CircleDomainRigidity.HalfPlaneRay.boundary_right line 14
  2. theorem OAI.CircleDomainRigidity.earlier_crosscut_in_later_filling line 27
  3. theorem OAI.CircleDomainRigidity.translated_rightSide_antitone line 46
  4. theorem OAI.CircleDomainRigidity.rayRightIndices_downward line 81
  5. theorem OAI.CircleDomainRigidity.mem_rayRightIndices_iff_le line 93