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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The terminal certificate for a finite state is either a required edge whose outside parameter zero is forbidden, or an excessive packing.

  1. structure OAI.CycleClique.Construction.BadData line 10
  2. def OAI.CycleClique.Construction.BadData.Check line 15
  3. instance OAI.CycleClique.Construction.(instance at line 21) line 21
  4. theorem OAI.CycleClique.Construction.BadData.false_of_check line 28