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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite extension templates preserve their three numerical parameters when transported to the counterexample graph.

  1. def OAI.CycleClique.Construction.OutsideTemplate.embed line 13
  2. theorem OAI.CycleClique.Construction.OutsideTemplate.embed_oldVertices line 45
  3. theorem OAI.CycleClique.Construction.OutsideTemplate.embed_amount line 52
  4. theorem OAI.CycleClique.Construction.OutsideTemplate.embed_incidentBound line 59
  5. theorem OAI.CycleClique.Construction.OutsideTemplate.embed_assignedCount line 66