OAI/Probability/SLE/Stochastic/PlanarDiskImage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A continuous injection of a closed planar disk contains a neighborhood of its center image. The proof uses exponential-covering homotopy lifting.

  1. lemma OAI.SLEExactGauge.planar_closedBall_image_contains_ball line 13