OAI/Probability/SLE/Geometry/EndpointClusterLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A bounded continuous real path has an endpoint limit when its cluster values contain no nontrivial interval.

  1. theorem OAI.SLEExactGauge.exists_endpoint_limit_of_no_cluster_interval line 14