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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform packings used in the first three terminal cases. Their graph premises concern actual balls and forbidden outside paths.

  1. theorem OAI.CycleClique.Construction.radius_two_triple_of_separated_first_pair line 14
  2. theorem OAI.CycleClique.Construction.radius_two_packing_bound line 41
  3. theorem OAI.CycleClique.Construction.terminal_uniform_packing_contradiction line 57
  4. theorem OAI.CycleClique.Construction.terminal_mixed_packing_contradiction line 77