OAI/Analysis/CircleDomains/Selection/GeometricIndexLocal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Local constancy of the greatest-translate index follows from the common finite strip bound and local constancy of each of the finitely many relevant sides.

  1. abbrev OAI.CircleDomainRigidity.RayIndexDomain line 14
  2. def OAI.CircleDomainRigidity.rayIndexSide line 17
  3. theorem OAI.CircleDomainRigidity.isLocallyConstant_rayIndexSide line 23
  4. theorem OAI.CircleDomainRigidity.rayIndexSide_eq_true_iff line 31
  5. theorem OAI.CircleDomainRigidity.isLocallyConstant_geometricRayIndex line 37