OAI/Probability/SLE/Loewner/RealBoundaryTraceAvoidance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A regular real characteristic excludes an entire neighborhood from the perturbed trace, including its real boundary points.

  1. theorem OAI.SLEExactGauge.real_boundary_driver_trace_avoidance line 13