OAI/Analysis/CircleDomains/Transfer/LogarithmicCutCharts.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Two explicit argument cuts give local logarithmic branches on any topological source of a continuous punctured-disk map. No local connectedness of the source is needed for this chart construction.

  1. def OAI.CircleDomainRigidity.logarithmicCutChart line 16
  2. theorem OAI.CircleDomainRigidity.logarithmicCutChart_nonneg line 20
  3. theorem OAI.CircleDomainRigidity.logarithmicCutChart_projection line 28
  4. theorem OAI.CircleDomainRigidity.continuousAt_logarithmicCutChart line 46
  5. def OAI.CircleDomainRigidity.logarithmicCutDomain line 56
  6. theorem OAI.CircleDomainRigidity.isOpen_logarithmicCutDomain line 59
  7. theorem OAI.CircleDomainRigidity.logarithmicCutDomain_cover line 69