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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Representatives: each chain start, and the first vertex following every nonterminal clique vertex in the oriented expanded chain.

  1. def OAI.CycleClique.Construction.representativesFrom line 13
  2. def OAI.CycleClique.Construction.chainRepresentatives line 17
  3. theorem OAI.CycleClique.Construction.representativesFrom_sublist line 21
  4. theorem OAI.CycleClique.Construction.chainRepresentatives_sublist line 31
  5. theorem OAI.CycleClique.Construction.chainCliqueCount_cons line 36
  6. theorem OAI.CycleClique.Construction.representativesFrom_length line 41
  7. theorem OAI.CycleClique.Construction.chainRepresentatives_length line 56
  8. def OAI.CycleClique.Construction.RawPathSystem.representatives line 68
  9. theorem OAI.CycleClique.Construction.RawPathSystem.representatives_sublist line 71
  10. theorem OAI.CycleClique.Construction.RawPathSystem.representatives_nodup line 82
  11. theorem OAI.CycleClique.Construction.RawPathSystem.representatives_length line 85
  12. theorem OAI.CycleClique.Construction.RawPathSystem.completeClique_representatives_length line 95