OAI/Computability/PerfectCompleteness/Decoding/CleanRecordProjection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.CleanRecordProjection.sourceProjection_congr line 23
2. theorem OAI.PerfectCompleteness.CleanRecordProjection.sourceProjection_tree line 32
3. theorem OAI.PerfectCompleteness.CleanRecordProjection.insideProjection_heq line 41
4. theorem OAI.PerfectCompleteness.CleanRecordProjection.fillProjection_congr line 92
5. theorem OAI.PerfectCompleteness.CleanRecordProjection.fillProjection_heq line 108
6. theorem OAI.PerfectCompleteness.CleanRecordProjection.decoderProjection_heq line 131