OAI/Analysis/CircleDomains/Selection/RankedRecursiveEndpoints.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Endpoint-law recursion with the inherited order on the selected levels. The positive-law construction and disk-crossing input are unchanged.

  1. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.ranked_countable_contacts line 17
  2. theorem OAI.CircleDomainRigidity.ranked_countable_recursive_code_laws line 101
  3. theorem OAI.CircleDomainRigidity.ranked_countable_endpoints_of_recursive_selection line 145
  4. theorem OAI.CircleDomainRigidity.ranked_countable_unavailable_endpoints_for_levels line 187