OAI/Analysis/CircleDomains/Selection/CountablePriorRecursion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recursive selection with every strict predecessor retained. The later law construction instantiates this with a well-order whose initial segments are countable, so all earlier laws are among its prescribed constraints.

  1. theorem OAI.CircleDomainRigidity.exists_prior_compatible_family line 15