OAI/Probability/SLE/Geometry/DiskCrosscutClosedRegions.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The closures of the two disk crosscut regions cover the closed disk and meet exactly along the crosscut.

  1. theorem OAI.SLEExactGauge.disk_crosscut_lower_jordan line 13
  2. lemma OAI.SLEExactGauge.complexInside_not_mem line 39
  3. theorem OAI.SLEExactGauge.disk_crosscut_closed_regions line 43