OAI/Computability/PerfectCompleteness/Sampling/WholeArrayBucketsLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PerfectCompleteness.WholeArrayBucketsLaw.reorder line 17
2. theorem OAI.PerfectCompleteness.WholeArrayBucketsLaw.product_reorder line 23
3. theorem OAI.PerfectCompleteness.WholeArrayBucketsLaw.product_swap line 31
4. theorem OAI.PerfectCompleteness.WholeArrayBucketsLaw.product_readout_swap line 39
5. def OAI.PerfectCompleteness.WholeArrayBucketsLaw.split line 56
6. theorem OAI.PerfectCompleteness.WholeArrayBucketsLaw.split_fst line 66
7. theorem OAI.PerfectCompleteness.WholeArrayBucketsLaw.split_snd line 73
8. theorem OAI.PerfectCompleteness.WholeArrayBucketsLaw.split_law line 80
9. def OAI.PerfectCompleteness.WholeArrayBucketsLaw.readout line 107
10. theorem OAI.PerfectCompleteness.WholeArrayBucketsLaw.readout_law line 117