OAI/Combinatorics/IndependentSets/PCP/FinalCNF.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.finalCNF line 16
2. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.finalCNF_satisfiable_iff line 19
3. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.finalCNF_clause_count line 24
4. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.finalCNF_variable_count line 28
5. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.finalCNF_nonempty line 32
6. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.finalCNF_gap line 39
7. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.finalCNF_clauseGap line 51
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.finalCNF_total_size line 57
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.finalCNF_polynomial_size line 74