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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

If all vertices of a layer subgraph share one predecessor, a long path closes through it.

  1. theorem OAI.CycleClique.Construction.layer_cycle_of_one_predecessor line 9