OAI/Analysis/CircleDomains/Probability/PriorLawPresentation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The countable data attached to a recursion stage: every earlier law is retained, its hit support has finite deletions, and every required dust mark is among the marks prescribed to the next positive-law construction.

  1. structure OAI.CircleDomainRigidity.PriorLawPresentation line 17
  2. theorem OAI.CircleDomainRigidity.nonempty_priorLawPresentation line 33