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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The first common ancestor of a set in one distance layer determines two branches.

  1. theorem OAI.CycleClique.Construction.exists_bfs_branch_partition line 8