OAI/Combinatorics/IndependentSets/Repetition/RevealFactorization.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Repetition.revealLeftFactor line 17
2. def OAI.IndependentSetsGames.Foundations.Repetition.revealRightFactor line 22
3. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealLeftFactor_nonnegative line 28
4. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealRightFactor_nonnegative line 35
5. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealLaw_factorization line 41
6. def OAI.IndependentSetsGames.Foundations.Repetition.partialLeftFactor line 56
7. def OAI.IndependentSetsGames.Foundations.Repetition.partialRightFactor line 60
8. theorem OAI.IndependentSetsGames.Foundations.Repetition.partialRevealWeight_factorization line 64
9. def OAI.IndependentSetsGames.Foundations.Repetition.completionTupleEquiv line 87
10. def OAI.IndependentSetsGames.Foundations.Repetition.updatedTableFallback line 93
11. theorem OAI.IndependentSetsGames.Foundations.Repetition.updatedTableFallback_zero line 98
12. theorem OAI.IndependentSetsGames.Foundations.Repetition.normalizeOr_weight_eq_zero_of_zero line 110
13. def OAI.IndependentSetsGames.Foundations.Repetition.selectedLeftRaw line 127
14. def OAI.IndependentSetsGames.Foundations.Repetition.selectedRightRaw line 135
15. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedLeftRaw_nonnegative line 144
16. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedRightRaw_nonnegative line 157
17. def OAI.IndependentSetsGames.Foundations.Repetition.selectedLeftCompletion line 169
18. def OAI.IndependentSetsGames.Foundations.Repetition.selectedRightCompletion line 178
19. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedLeftCompletion_zero line 188
20. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedRightCompletion_zero line 199
21. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedLeftCompletion_support line 210
22. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedRightCompletion_support line 220
23. def OAI.IndependentSetsGames.Foundations.Repetition.selectedCompletionScale line 229
24. theorem OAI.IndependentSetsGames.Foundations.Repetition.selected_completion_factorization line 238
25. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedCommonLaw_completion_row_mass line 263
26. theorem OAI.IndependentSetsGames.Foundations.Repetition.selected_completion_row_recombine line 285