OAI/Probability/SLE/Geometry/HalfDiskGeometry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The two standard closed half disks and their bounded Jordan interiors.

  1. def OAI.SLEExactGauge.closedUpperDisk line 13
  2. def OAI.SLEExactGauge.openUpperDisk line 14
  3. lemma OAI.SLEExactGauge.closedUpperDisk_eq line 16
  4. lemma OAI.SLEExactGauge.closedUpperDisk_isClosed line 21
  5. lemma OAI.SLEExactGauge.closedUpperDisk_convex line 25
  6. lemma OAI.SLEExactGauge.closedUpperDisk_interior line 29
  7. lemma OAI.SLEExactGauge.openUpperDisk_nonempty line 35
  8. lemma OAI.SLEExactGauge.openUpperDisk_isOpen line 40
  9. lemma OAI.SLEExactGauge.openUpperDisk_convex line 44
  10. lemma OAI.SLEExactGauge.openUpperDisk_closure line 48
  11. lemma OAI.SLEExactGauge.openUpperDisk_frontier line 54
  12. theorem OAI.SLEExactGauge.complexInside_upperDisk line 70