OAI/Combinatorics/Ramsey/CycleClique/BreadthFirst.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CycleClique.exists_distance_predecessor line 9
  2. structure OAI.CycleClique.BreadthFirstParent line 29
  3. theorem OAI.CycleClique.exists_breadthFirstParent line 35
  4. theorem OAI.CycleClique.BreadthFirstParent.iterate_depth line 47
  5. theorem OAI.CycleClique.BreadthFirstParent.exists_upward_walk line 65
  6. def OAI.CycleClique.layerAncestor line 101
  7. theorem OAI.CycleClique.layerAncestor_depth line 105
  8. theorem OAI.CycleClique.layerAncestor_self line 113
  9. theorem OAI.CycleClique.layerAncestor_root line 117
  10. theorem OAI.CycleClique.layerAncestor_coherent line 124
  11. theorem OAI.CycleClique.exists_ancestor_path line 134
  12. theorem OAI.CycleClique.exists_layer_split line 152
  13. theorem OAI.CycleClique.path_start_not_mem_tail line 182
  14. theorem OAI.CycleClique.exists_branch_path line 190
  15. theorem OAI.CycleClique.cycle_of_layer_path line 240