OAI/Analysis/CircleDomains/Probability/CountableRecursiveLaws.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Applying the crossing countability theorem to the recursively retained laws. The earlier-law lookup is the only ordering information required.

  1. theorem OAI.CircleDomainRigidity.countable_recursive_code_laws line 19