OAI/Analysis/CircleDomains/Probability/CountableCollarLaws.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The common-collar contradiction for a linearly ordered family of actual path laws. The hypotheses retain the original quantitative meeting estimate.

  1. theorem OAI.CircleDomainRigidity.countable_of_uniformly_small_collar_meetings line 21