OAI/Probability/SLE/Geometry/ConjugateInversionChart.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Conjugate inversion identifies the upper half of the punctured disk with the upper exterior disk.

  1. lemma OAI.SLEExactGauge.norm_conjugateInversion line 14
  2. lemma OAI.SLEExactGauge.conjugateInversion_injective line 17
  3. lemma OAI.SLEExactGauge.conjugateInversion_disk_upper_bijOn line 20
  4. lemma OAI.SLEExactGauge.conjugateInversion_slit_bijOn line 39