OAI/Combinatorics/IndependentSets/Fourier/LocalEquations.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.localAddress line 14
2. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.localAddress_injective line 21
3. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.conditionedOccurrence line 46
4. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.conditionedOccurrence_satisfied line 55
5. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.findValid line 84
6. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.findValid_none_iff line 88
7. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.firstValid line 97
8. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.firstValid_none_iff line 100
9. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.occurrenceList line 105
10. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.occurrenceList_length line 108
11. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.countP_cast_eq_sum line 112
12. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.countP_enumerate line 118
13. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.occurrenceList_acceptance line 125