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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A certificate for one use of the initial extension rule consists of old disjoint chains and two tails joined by the proposed outside path.

  1. structure OAI.CycleClique.Construction.OutsideTemplate line 12
  2. def OAI.CycleClique.Construction.OutsideTemplate.oldVertices line 28
  3. def OAI.CycleClique.Construction.OutsideTemplate.amount line 31
  4. def OAI.CycleClique.Construction.OutsideTemplate.assignedCount line 34
  5. def OAI.CycleClique.Construction.OutsideTemplate.incidentBound line 37
  6. theorem OAI.CycleClique.Construction.OutsideTemplate.forbids line 40