OAI/Computability/PerfectCompleteness/Decoding/ProjectedNativeCollision.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.ProjectedNativeCollision.form_eq_on_pullbacks line 25
2. theorem OAI.PerfectCompleteness.ProjectedNativeCollision.decode_eq_some_of_high line 51
3. theorem OAI.PerfectCompleteness.ProjectedNativeCollision.two_high_hits_restricted line 59
4. theorem OAI.PerfectCompleteness.ProjectedNativeCollision.two_high_hits_restricted_on line 85
5. theorem OAI.PerfectCompleteness.ProjectedNativeCollision.parent_childSlots_of_unmarked line 119
6. theorem OAI.PerfectCompleteness.ProjectedNativeCollision.parent_unmarked_le_range line 130