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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A C5-free graph with singleton expansion cannot contain a four-clique at order at most 17.

  1. theorem OAI.CycleClique.Construction.exterior_unique_clique_neighbor line 8
  2. theorem OAI.CycleClique.Construction.fiveCycle_fourClique_impossible line 19