OAI/Combinatorics/Chromatic/Witness/HistoryMainWitness.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.NaturalUnitIntervalGraph.historyWitness line 9
2. abbrev OAI.ElementaryPositivity.FiniteSearch.Row line 19
3. def OAI.ElementaryPositivity.FiniteSearch.rowPartition line 21
4. lemma OAI.ElementaryPositivity.FiniteSearch.rowPartition_surjective line 24
5. abbrev OAI.ElementaryPositivity.FiniteSearch.Table line 71
6. def OAI.ElementaryPositivity.FiniteSearch.WordOK line 73
7. instance OAI.ElementaryPositivity.FiniteSearch.(instance at line 75) line 75
8. def OAI.ElementaryPositivity.FiniteSearch.wordEnergy line 79
9. def OAI.ElementaryPositivity.FiniteSearch.colorCount line 83
10. def OAI.ElementaryPositivity.FiniteSearch.matrixCount line 86
11. def OAI.ElementaryPositivity.FiniteSearch.witnessCount line 90
12. def OAI.ElementaryPositivity.FiniteSearch.Test line 93
13. instance OAI.ElementaryPositivity.FiniteSearch.(instance at line 95) line 95
14. def OAI.ElementaryPositivity.FiniteSearch.rowProfile line 109
15. lemma OAI.ElementaryPositivity.FiniteSearch.rowProfile_degree line 110
16. lemma OAI.ElementaryPositivity.FiniteSearch.rowPartition_eq_profile line 113
17. lemma OAI.ElementaryPositivity.FiniteSearch.matrix_coefficient line 115
18. lemma OAI.ElementaryPositivity.FiniteSearch.chromatic_coefficient line 128
19. lemma OAI.ElementaryPositivity.FiniteSearch.chromatic_degree_zero line 146
20. def OAI.ElementaryPositivity.FiniteSearch.wordEquiv line 157
21. lemma OAI.ElementaryPositivity.FiniteSearch.witness_coefficient line 163
22. lemma OAI.ElementaryPositivity.FiniteSearch.row_degree_zero line 184
23. lemma OAI.ElementaryPositivity.FiniteSearch.colorCount_zero_high line 189
24. lemma OAI.ElementaryPositivity.FiniteSearch.witnessCount_zero_high line 197