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

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Raw chain collections used during representative surgery. Isolated clique vertices and empty pieces are allowed until normalization.

  1. structure OAI.CycleClique.Construction.RawPathSystem line 12
  2. def OAI.CycleClique.Construction.RawPathSystem.normalize line 23
  3. def OAI.CycleClique.Construction.RawPathSystem.vertices line 26
  4. def OAI.CycleClique.Construction.RawPathSystem.amount line 30
  5. def OAI.CycleClique.Construction.RawPathSystem.assignedCount line 34
  6. theorem OAI.CycleClique.Construction.RawPathSystem.flatten_nodup line 37
  7. theorem OAI.CycleClique.Construction.RawPathSystem.normalize_amount line 40
  8. theorem OAI.CycleClique.Construction.RawPathSystem.normalize_assignedCount line 45
  9. def OAI.CycleClique.Construction.ExpandedPathSystem.toRaw line 53
  10. theorem OAI.CycleClique.Construction.ExpandedPathSystem.toRaw_amount line 60
  11. theorem OAI.CycleClique.Construction.ExpandedPathSystem.toRaw_assignedCount line 62