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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An additional excluded vertex outside the representative set forces the first ball to exceed the maximum clique size.

  1. theorem OAI.CycleClique.Construction.representative_ball_one_extra line 13
  2. theorem OAI.CycleClique.Construction.representative_ball_one_not_clique line 60