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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Transport a finite chain certificate through an injective graph embedding.

  1. theorem OAI.CycleClique.Construction.chainCliqueCount_map line 12
  2. theorem OAI.CycleClique.Construction.chainOutsideCount_map line 19
  3. def OAI.CycleClique.Construction.RawPathSystem.embed line 30
  4. theorem OAI.CycleClique.Construction.RawPathSystem.embed_amount line 59
  5. theorem OAI.CycleClique.Construction.RawPathSystem.embed_assignedCount line 68
  6. theorem OAI.CycleClique.Construction.RawPathSystem.embed_normalize_incident line 75
  7. theorem OAI.CycleClique.Construction.RawPathSystem.normalize_incident_le line 85