OAI/Probability/SLE/Geometry/LocalLogObstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A locally injective isolated zero has nontrivial boundary monodromy. This is the local obstruction used for separating the sides of a crosscut.

  1. lemma OAI.SLEExactGauge.univalent_boundary_no_continuous_log line 13
  2. lemma OAI.SLEExactGauge.isolated_zero_no_continuous_boundary_log line 52