OAI/Combinatorics/IndependentSets/Fourier/Gap.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Hastad.SourceGap.ClauseGap line 15
2. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGap.third_pos line 20
3. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGap.third_le_one line 22
4. def OAI.IndependentSetsGames.Foundations.Hastad.SourceGap.repetitionCount line 24
5. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGap.repetitionCount_pos line 28
6. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGap.repeated_game_bound line 33
7. def OAI.IndependentSetsGames.Foundations.Hastad.SourceGap.source line 49
8. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGap.source_complete line 53
9. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGap.source_sound line 66
10. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGap.source_size line 77
11. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceNonempty.real_clause_gap_of_count line 90
12. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceNonempty.clauseGap_of_count line 104
13. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceNonempty.cnf_nonempty_of_nonempty_darts line 115
14. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceNonempty.cnf_clauseGap line 124
15. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceNonempty.cnf_clauseGap_unit line 136