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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Soundness of a finite list of explicit extension certificates, with both orientations of every forbidden outside path inserted in the matrix.

  1. def OAI.CycleClique.Construction.templateEntryMatrix line 11
  2. def OAI.CycleClique.Construction.templateMatrix line 14
  3. theorem OAI.CycleClique.Construction.templateMatrix_sound line 21