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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Every actual path system has a representative in the finite canonical amount domain: reverse components into lexicographic order, then sort them.

  1. theorem OAI.CycleClique.Construction.lexLE_iff_le line 10
  2. def OAI.CycleClique.Construction.orientAmounts line 14
  3. def OAI.CycleClique.Construction.canonicalAmounts line 16
  4. theorem OAI.CycleClique.Construction.orientAmounts_length line 19
  5. theorem OAI.CycleClique.Construction.orientAmounts_sum line 23
  6. theorem OAI.CycleClique.Construction.orientAmounts_reverse line 27
  7. theorem OAI.CycleClique.Construction.orientAmounts_positive line 35
  8. theorem OAI.CycleClique.Construction.canonicalAmounts_perm line 43
  9. theorem OAI.CycleClique.Construction.canonicalAmounts_vertices line 46
  10. theorem OAI.CycleClique.Construction.canonicalAmounts_amount line 52
  11. theorem OAI.CycleClique.Construction.canonicalAmounts_pairwise line 58
  12. theorem OAI.CycleClique.Construction.patternValid_of_pairwise line 67
  13. theorem OAI.CycleClique.Construction.canonicalAmounts_valid line 80
  14. theorem OAI.CycleClique.Construction.canonicalAmounts_mem line 95
  15. theorem OAI.CycleClique.Construction.ExpandedPathSystem.exists_canonical_profile line 107