OAI/Computability/VertexCover/Repetition/SelectedCompletion.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.Repetition.completionTupleEquiv line 53
2. def OAI.UniqueGames.Foundations.Repetition.updatedTableFallback line 59
3. theorem OAI.UniqueGames.Foundations.Repetition.updatedTableFallback_zero line 64
4. theorem OAI.UniqueGames.Foundations.Repetition.normalizeOr_weight_eq_zero_of_zero line 76
5. def OAI.UniqueGames.Foundations.Repetition.selectedLeftRaw line 93
6. def OAI.UniqueGames.Foundations.Repetition.selectedRightRaw line 101
7. theorem OAI.UniqueGames.Foundations.Repetition.selectedLeftRaw_nonnegative line 110
8. theorem OAI.UniqueGames.Foundations.Repetition.selectedRightRaw_nonnegative line 123
9. def OAI.UniqueGames.Foundations.Repetition.selectedLeftCompletion line 135
10. def OAI.UniqueGames.Foundations.Repetition.selectedRightCompletion line 144
11. theorem OAI.UniqueGames.Foundations.Repetition.selectedLeftCompletion_zero line 154
12. theorem OAI.UniqueGames.Foundations.Repetition.selectedRightCompletion_zero line 165
13. theorem OAI.UniqueGames.Foundations.Repetition.selectedLeftCompletion_support line 176
14. theorem OAI.UniqueGames.Foundations.Repetition.selectedRightCompletion_support line 186
15. def OAI.UniqueGames.Foundations.Repetition.selectedCompletionScale line 195
16. theorem OAI.UniqueGames.Foundations.Repetition.selected_completion_factorization line 204
17. theorem OAI.UniqueGames.Foundations.Repetition.selectedCommonLaw_completion_row_mass line 228
18. theorem OAI.UniqueGames.Foundations.Repetition.selected_completion_row_recombine line 250