OAI/Probability/SLE/Geometry/SchoenfliesInsideTransport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Plane homeomorphisms preserve the bounded complementary region. This identifies the side selected by a relative Schoenflies extension.

  1. lemma OAI.SLEExactGauge.plane_homeomorph_bounded_image line 12
  2. lemma OAI.SLEExactGauge.plane_homeomorph_bounded_image_iff line 17
  3. theorem OAI.SLEExactGauge.plane_homeomorph_inside line 23
  4. theorem OAI.SLEExactGauge.plane_homeomorph_jordan line 49
  5. theorem OAI.SLEExactGauge.separating_inside_eq_open line 59