OAI/Analysis/CircleDomains/Topology/DiskArcIndex.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An explicit index for an arc from the unit circle to the origin. The reference argument at the starting point uses the radial contraction inside the disk. The resulting real expression is an integer and gains one under a deck translation.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.diskInitialArgument line 16
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.diskInitialArgument_projects line 19
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuousAt_diskInitialArgument line 29
  4. def OAI.CircleDomainRigidity.FiniteTransfer.diskArcIndex line 41
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.diskArcIndex_integer line 44
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.diskArcIndex_translate line 67