OAI/Combinatorics/EuclideanRamsey/PathWords.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.EuclideanRamsey.LetterGroup line 28
2. inductive OAI.EuclideanRamsey.UnitWords line 31
3. def OAI.EuclideanRamsey.unitGraded line 36
4. def OAI.EuclideanRamsey.CopyPath line 41
5. inductive OAI.EuclideanRamsey.Path line 44
6. lemma OAI.EuclideanRamsey.UnitWords.path line 49
7. lemma OAI.EuclideanRamsey.Path.nonneg line 55
8. lemma OAI.EuclideanRamsey.extend_pair_E line 61
9. lemma OAI.EuclideanRamsey.unit_pair_inverse line 74
10. def OAI.EuclideanRamsey.pairHom line 97
11. def OAI.EuclideanRamsey.pairGroup line 102
12. lemma OAI.EuclideanRamsey.pairGroup_diag line 114
13. def OAI.EuclideanRamsey.pairLeft line 119
14. instance OAI.EuclideanRamsey.pairLeft_normal line 121
15. lemma OAI.EuclideanRamsey.pairLeft_edge line 131
16. lemma OAI.EuclideanRamsey.unit_pair_coverage line 142
17. abbrev OAI.EuclideanRamsey.Strings line 168
18. def OAI.EuclideanRamsey.stringEnergy line 170
19. lemma OAI.EuclideanRamsey.stringEnergy_self line 173
20. lemma OAI.EuclideanRamsey.stringEnergy_append line 177
21. lemma OAI.EuclideanRamsey.stringEnergy_eq_sum line 188
22. lemma OAI.EuclideanRamsey.flatten_energy line 202
23. def OAI.EuclideanRamsey.StringFamily line 207
24. lemma OAI.EuclideanRamsey.StringFamily.common line 210
25. lemma OAI.EuclideanRamsey.StringFamily.single line 212
26. lemma OAI.EuclideanRamsey.StringFamily.mul line 218
27. lemma OAI.EuclideanRamsey.StringFamily.congruent line 227