OAI/Analysis/CircleDomains/Topology/LogarithmicDiskLift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual continuous logarithmic lifts on simply connected physical patches. The real coordinate is obtained from the existing circle cover.

  1. theorem OAI.CircleDomainRigidity.exists_logarithmic_disk_lift line 16
  2. theorem OAI.CircleDomainRigidity.exists_logarithmic_disk_lift_ball line 48