OAI/Computability/PerfectCompleteness/Sampling/BucketDescriptorLaw.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.BucketDescriptorLaw.Buckets line 16
  2. abbrev OAI.PerfectCompleteness.BucketDescriptorLaw.Record line 18
  3. def OAI.PerfectCompleteness.BucketDescriptorLaw.bucketLaw line 22
  4. def OAI.PerfectCompleteness.BucketDescriptorLaw.sampleLaw line 26
  5. def OAI.PerfectCompleteness.BucketDescriptorLaw.observe line 30
  6. def OAI.PerfectCompleteness.BucketDescriptorLaw.reorder line 33
  7. theorem OAI.PerfectCompleteness.BucketDescriptorLaw.reorder_law line 40
  8. theorem OAI.PerfectCompleteness.BucketDescriptorLaw.observe_law line 55
  9. def OAI.PerfectCompleteness.BucketDescriptorLaw.sampleEquiv line 84
  10. def OAI.PerfectCompleteness.BucketDescriptorLaw.recordEquiv line 88
  11. theorem OAI.PerfectCompleteness.BucketDescriptorLaw.bucketLaw_equiv line 91
  12. theorem OAI.PerfectCompleteness.BucketDescriptorLaw.sampleLaw_equiv line 102
  13. theorem OAI.PerfectCompleteness.BucketDescriptorLaw.reference_equiv line 118
  14. theorem OAI.PerfectCompleteness.BucketDescriptorLaw.observe_equiv_law line 134