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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Equivalence between labelled cycles and copies of the Mathlib cycle graph.

  1. theorem OAI.CycleClique.Construction.hasCycle_iff_copy line 12
  2. theorem OAI.CycleClique.Construction.hasIndependent_iff_copy line 35
  3. theorem OAI.CycleClique.Construction.ramseyProperty_iff line 50
  4. theorem OAI.CycleClique.Construction.isRamseyNumber_iff line 55