OAI/Analysis/CircleDomains/Probability/CountableCodedCollarLaws.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The common-collar argument with the varying base-code spaces retained. Earlier-law constraints change those spaces during the transfinite recursion.

  1. theorem OAI.CircleDomainRigidity.countable_of_uniformly_small_coded_collar_meetings line 17