OAI/Combinatorics/Ramsey/CycleClique/ColouredPaths.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CycleClique.exists_common_neighbor_different_colours line 9
2. theorem OAI.CycleClique.exists_longest_path_from line 40
3. theorem OAI.CycleClique.longest_path_endpoint_neighbors line 55
4. theorem OAI.CycleClique.different_colour_prefix line 67
5. theorem OAI.CycleClique.path_rotation_prefix line 94
6. theorem OAI.CycleClique.path_rotation line 116
7. def OAI.CycleClique.pathEnds line 124
8. theorem OAI.CycleClique.mem_pathEnds_support line 127
9. theorem OAI.CycleClique.pathEnds_no_start line 132
10. theorem OAI.CycleClique.successor_mem_pathEnds line 141
11. theorem OAI.CycleClique.degree_le_card_pathEnds line 150
12. theorem OAI.CycleClique.pathEnds_neighbors line 185
13. theorem OAI.CycleClique.pathEnds_isClique line 200
14. theorem OAI.CycleClique.pathEnds_successor_closed line 231
15. theorem OAI.CycleClique.pathEnds_final_segment line 243
16. theorem OAI.CycleClique.pathEnd_ordering_preserving_prefix line 271
17. theorem OAI.CycleClique.pathEnd_attachment_of_common_prefix line 300
18. theorem OAI.CycleClique.pathEnds_partial_attachment line 333
19. theorem OAI.CycleClique.pathEnds_attachment_of_two_entries line 349
20. def OAI.CycleClique.within line 381
21. theorem OAI.CycleClique.within_le line 386
22. theorem OAI.CycleClique.within_support line 389
23. def OAI.CycleClique.walkWithin line 401
24. theorem OAI.CycleClique.walkWithin_support line 408
25. theorem OAI.CycleClique.deleted_component line 417
26. theorem OAI.CycleClique.ncard_neighborSet line 445
27. theorem OAI.CycleClique.degree_add_one_le_of_neighbors_subset line 450
28. theorem OAI.CycleClique.adj_of_neighbors_subset_of_card line 463
29. theorem OAI.CycleClique.clique_ncard_lt line 482
30. theorem OAI.CycleClique.degree_le_add_two_of_boundary line 496
31. theorem OAI.CycleClique.exists_mem_ne_of_ncard line 513
32. theorem OAI.CycleClique.endpoint_clique_two_entries line 524
33. theorem OAI.CycleClique.endpoint_clique_common_neighbor line 611
34. theorem OAI.CycleClique.path_avoids_attached_set line 680
35. theorem OAI.CycleClique.reachable_after_removing_attached_set line 700
36. theorem OAI.CycleClique.deletion_component_card line 714
37. theorem OAI.CycleClique.closedNeighborhood_within_boundary line 785
38. theorem OAI.CycleClique.clique_path_between line 799
39. theorem OAI.CycleClique.join_disjoint_paths line 852
40. theorem OAI.CycleClique.attached_clique_long_path line 865
41. theorem OAI.CycleClique.coloured_path line 964
42. theorem OAI.CycleClique.colouredPathTarget_proved line 1082