OAI/Probability/SLE/Geometry/ReflectedInvertedUpperConnected.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The upper component of the inverted reflected-slit domain is a conjugate-inversion image of the original half-plane slit domain.

  1. def OAI.SLEExactGauge.conjugateInversion line 13
  2. lemma OAI.SLEExactGauge.conjugateInversion_involutive line 15
  3. lemma OAI.SLEExactGauge.conjugateInversion_upper line 19
  4. theorem OAI.SLEExactGauge.reflected_inverted_upper_image line 28
  5. theorem OAI.SLEExactGauge.reflected_inverted_upper_connected line 69