OAI/Analysis/CircleDomains/Topology/DiskRayLift.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A continuous lift of each actual terminal arc to angular and logarithmic coordinates. The angular origin is the representative of the arc start.

  1. abbrev OAI.CircleDomainRigidity.DiskRayTime line 15
  2. def OAI.CircleDomainRigidity.diskRayAngle line 17
  3. theorem OAI.CircleDomainRigidity.diskRayAngle_eq_increment line 21
  4. theorem OAI.CircleDomainRigidity.continuous_diskRayAngle line 33
  5. theorem OAI.CircleDomainRigidity.diskRayAngle_projects line 46
  6. theorem OAI.CircleDomainRigidity.diskRayAngle_mul_prefix line 52
  7. theorem OAI.CircleDomainRigidity.diskRay_nonzero line 69
  8. def OAI.CircleDomainRigidity.diskRayDepth line 75
  9. theorem OAI.CircleDomainRigidity.continuous_diskRayDepth line 77
  10. def OAI.CircleDomainRigidity.diskRayLift line 82
  11. theorem OAI.CircleDomainRigidity.diskRayLift_injective line 87