OAI/Combinatorics/Chromatic/Histories/PacketSortedWords.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.Packets.rows line 15
2. lemma OAI.ElementaryPositivity.Packets.sorted_injOn line 17
3. lemma OAI.ElementaryPositivity.Packets.rows_card line 25
4. def OAI.ElementaryPositivity.Packets.wordCount line 28
5. lemma OAI.ElementaryPositivity.Packets.wordCount_apply line 30
6. lemma OAI.ElementaryPositivity.Packets.wordCount_degree line 33
7. lemma OAI.ElementaryPositivity.Packets.rows_colCount line 37
8. abbrev OAI.ElementaryPositivity.Packets.SortedWord line 43
9. abbrev OAI.ElementaryPositivity.Packets.RowFamily line 44
10. def OAI.ElementaryPositivity.Packets.fromRows line 46
11. lemma OAI.ElementaryPositivity.Packets.fromRows_mem line 50
12. lemma OAI.ElementaryPositivity.Packets.fromRows_at line 54
13. lemma OAI.ElementaryPositivity.Packets.fromRows_sorted line 63
14. lemma OAI.ElementaryPositivity.Packets.rows_fromRows line 70
15. lemma OAI.ElementaryPositivity.Packets.sorted_rows_unique line 87
16. def OAI.ElementaryPositivity.Packets.rowsEquiv line 102
17. def OAI.ElementaryPositivity.Packets.packetProfile line 118
18. lemma OAI.ElementaryPositivity.Packets.packetProfile_apply line 119
19. lemma OAI.ElementaryPositivity.Packets.packetProfile_degree line 121
20. lemma OAI.ElementaryPositivity.Packets.anchor_required_iff line 124
21. abbrev OAI.ElementaryPositivity.Packets.AnchorWord line 133
22. abbrev OAI.ElementaryPositivity.Packets.RequiredAnchor line 134
23. abbrev OAI.ElementaryPositivity.Packets.PacketRows line 136
24. def OAI.ElementaryPositivity.Packets.anchorRowsEquiv line 139
25. lemma OAI.ElementaryPositivity.Packets.requiredAnchor_card line 164