OAI/Combinatorics/Ramsey/CycleClique/Construction/BfsParent.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A coherent choice of predecessors on shortest paths to a root.

  1. theorem OAI.CycleClique.Construction.exists_distance_predecessor line 8
  2. def OAI.CycleClique.Construction.bfsParent line 21
  3. theorem OAI.CycleClique.Construction.bfsParent_spec line 26
  4. theorem OAI.CycleClique.Construction.bfsParent_root line 34
  5. theorem OAI.CycleClique.Construction.bfsAncestor_level line 37
  6. theorem OAI.CycleClique.Construction.bfsAncestor_root line 53
  7. theorem OAI.CycleClique.Construction.bfsAncestor_adjacent line 62
  8. theorem OAI.CycleClique.Construction.bfsAncestor_injective line 69