OAI/Probability/SLE/Stochastic/PlanarRetractComplement.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A closed planar retract has no bounded complementary component, since the identity on a circle has no continuous logarithm.

  1. lemma OAI.SLEExactGauge.no_point_avoiding_identity_outside_ball line 13
  2. theorem OAI.SLEExactGauge.bounded_open_frontier_not_retract line 31
  3. lemma OAI.SLEExactGauge.frontier_connectedComponentIn_subset_compl line 57
  4. theorem OAI.SLEExactGauge.retract_complement_component_unbounded line 69