OAI/Probability/SLE/Geometry/ArcRealRetraction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A simple arc attached to the real axis is a retract together with that axis. The explicit formula collapses the two coordinates onto the three branches of the attached arc and real line.

  1. theorem OAI.SLEExactGauge.simple_arc_real_retraction line 15