OAI/Computability/PerfectCompleteness/Construction/CutBucketTransportLemmas.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PerfectCompleteness.CutBucketTransport.nativeLaw line 26
2. theorem OAI.PerfectCompleteness.CutBucketTransport.nativeLaw_pushforward line 37
3. theorem OAI.PerfectCompleteness.CutBucketTransportActual.tapeLaw_pushforward line 74
4. theorem OAI.PerfectCompleteness.CutBucketTransportActual.bucketSampleLaw_pushforward line 99
5. def OAI.PerfectCompleteness.CutBucketTransportActual.nativeLaw line 124
6. theorem OAI.PerfectCompleteness.CutBucketTransportActual.nativeLaw_pushforward line 134