OAI/Probability/SLE/Loewner/UnivalentLocallyUniformLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A nonconstant locally uniform limit of injective holomorphic maps is injective. Boundary separation and the minimum principle provide the local preimages needed for the proof.

  1. lemma OAI.SLEExactGauge.isolated_level_closedBall line 14
  2. lemma OAI.SLEExactGauge.tendstoLocallyUniformlyOn_injOn line 36