OAI/Computability/PerfectCompleteness/Decoding/CleanEndpointProjection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.CleanEndpointProjection.reconstruct_designated line 16
2. theorem OAI.PerfectCompleteness.CleanEndpointProjection.dite_heq_of_pos line 24
3. def OAI.PerfectCompleteness.CleanEndpointProjection.sourceProjection line 32
4. theorem OAI.PerfectCompleteness.CleanEndpointProjection.sourceProjection_of_true line 40
5. theorem OAI.PerfectCompleteness.CleanEndpointProjection.leftInside_designated line 52
6. theorem OAI.PerfectCompleteness.CleanEndpointProjection.rightInside_designated line 66
7. def OAI.PerfectCompleteness.CleanEndpointProjection.insideProjection line 78
8. theorem OAI.PerfectCompleteness.CleanEndpointProjection.insideProjection_designated line 100