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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Labelled subcollections of actual assigned paths, with their exact amount and number of paths. Labels distinguish paths of equal length.

  1. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.of_profiles line 17
  2. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.realize_labels line 24
  3. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.realize_sublist_of_perm line 46
  4. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.realize_labels_of_perm line 53
  5. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.labelled_fin_range line 74
  6. theorem OAI.CycleClique.Construction.RawPathSystem.exists_labelled_amounts line 102