OAI/Probability/SLE/Geometry/SimpleArcPlaneComplement.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A finite simple planar arc has connected complement. The argument uses its interval-coordinate retraction, the circle obstruction, and a large sphere meeting every unbounded complementary component.

  1. theorem OAI.SLEExactGauge.simple_arc_retraction line 15
  2. lemma OAI.SLEExactGauge.unbounded_component_meets_sphere line 32
  3. theorem OAI.SLEExactGauge.bounded_complement_connected_of_unbounded_components line 47
  4. theorem OAI.SLEExactGauge.simple_arc_plane_complement_connected line 90