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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The common-neighbour obstruction to a four-cycle gives sharp small pigeonhole bounds.

  1. theorem OAI.CycleClique.Construction.fourCycle_common_neighbors_unique line 8
  2. theorem OAI.CycleClique.Construction.fourCycle_common_neighbors_card line 14
  3. theorem OAI.CycleClique.Construction.fourCycle_three_representatives_bound line 22