OAI/Probability/SLE/Geometry/SimpleSlitConnected.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The domain left by an arbitrary finite simple attached arc is connected, and its complement is connected and unbounded. These are the topological inputs for constructing its normalized conformal charts.

  1. theorem OAI.SLEExactGauge.simple_arc_halfPlane_complement_connected line 13
  2. theorem OAI.SLEExactGauge.attached_arc_domain_complement_preconnected line 21
  3. theorem OAI.SLEExactGauge.attached_arc_domain_complement_unbounded line 33