OAI/Computability/PerfectCompleteness/Sampling/OriginalCutBucketLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.OriginalCutBucketLaw.reorder line 21
  2. theorem OAI.PerfectCompleteness.OriginalCutBucketLaw.reorder_law line 28
  3. theorem OAI.PerfectCompleteness.OriginalCutBucketLaw.map_middle line 43
  4. theorem OAI.PerfectCompleteness.OriginalCutBucketLaw.read_product_of_split line 61
  5. abbrev OAI.PerfectCompleteness.OriginalCutBucketLaw.Background line 83
  6. abbrev OAI.PerfectCompleteness.OriginalCutBucketLaw.NativeSample line 91
  7. def OAI.PerfectCompleteness.OriginalCutBucketLaw.read line 97
  8. def OAI.PerfectCompleteness.OriginalCutBucketLaw.recordRead line 107
  9. theorem OAI.PerfectCompleteness.OriginalCutBucketLaw.oldRecord_numberRecord line 115
  10. theorem OAI.PerfectCompleteness.OriginalCutBucketLaw.read_numberRecord line 122
  11. theorem OAI.PerfectCompleteness.OriginalCutBucketLaw.numbered_read_of_split line 141
  12. theorem OAI.PerfectCompleteness.OriginalCutBucketLaw.reference_read_law line 169
  13. theorem OAI.PerfectCompleteness.OriginalCutBucketLaw.record_fresh_read_law line 187