OAI/Computability/PerfectCompleteness/Sampling/ChildCallNumberingLaws.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ChildCallNumberingLaws.liftedLaw line 20
  2. theorem OAI.PerfectCompleteness.ChildCallNumberingLaws.liftedLaw_numbered line 27
  3. def OAI.PerfectCompleteness.ChildCallNumberingLaws.mixtureLaw line 37
  4. theorem OAI.PerfectCompleteness.ChildCallNumberingLaws.mixtureLaw_numbered line 45
  5. def OAI.PerfectCompleteness.ChildCallNumberingLaws.replacementLaws line 59
  6. def OAI.PerfectCompleteness.ChildCallNumberingLaws.number line 67
  7. def OAI.PerfectCompleteness.ChildCallNumberingLaws.unnumber line 73
  8. theorem OAI.PerfectCompleteness.ChildCallNumberingLaws.unnumber_number line 80
  9. theorem OAI.PerfectCompleteness.ChildCallNumberingLaws.number_unnumber line 88
  10. theorem OAI.PerfectCompleteness.ChildCallNumberingLaws.uniform_product_numbered line 95
  11. theorem OAI.PerfectCompleteness.ChildCallNumberingLaws.conditional_product_numbered line 107
  12. theorem OAI.PerfectCompleteness.ChildCallNumberingLaws.markedLaw_numbered line 131