OAI/Analysis/CircleDomains/Selection/FarRaySides.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform eventual values of the translated side functions on bounded rectangles of the half-plane. This gives the finite range of possible indices.

  1. theorem OAI.CircleDomainRigidity.HalfPlaneRay.side_eq_boundary_of_vertical_avoidance line 17
  2. theorem OAI.CircleDomainRigidity.translated_sides_eventually_fixed line 39