OAI/Combinatorics/CycleDecomposition/ScaleDecomposition.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ErdosGallai.Scale.graphUnion line 19
  2. lemma OAI.ErdosGallai.Scale.graphUnion_nil line 21
  3. lemma OAI.ErdosGallai.Scale.graphUnion_cons line 22
  4. lemma OAI.ErdosGallai.Scale.graphUnion_adj line 23
  5. lemma OAI.ErdosGallai.Scale.edgeOccurrences_pos line 29
  6. lemma OAI.ErdosGallai.Scale.graphPartition_union line 33
  7. lemma OAI.ErdosGallai.Scale.graphPartition_of_le_one line 39
  8. lemma OAI.ErdosGallai.Scale.edgeOccurrences_sublist line 46
  9. lemma OAI.ErdosGallai.Scale.graphPartition_sublist line 50
  10. lemma OAI.ErdosGallai.Scale.graphUnion_sublist line 58
  11. lemma OAI.ErdosGallai.Scale.graphUnion_append line 63
  12. lemma OAI.ErdosGallai.Scale.edgeOccurrences_perm line 68
  13. lemma OAI.ErdosGallai.Scale.graphPartition_perm line 71
  14. lemma OAI.ErdosGallai.Scale.graphUnion_supported line 77
  15. lemma OAI.ErdosGallai.Scale.edgeCount_union_le line 84
  16. def OAI.ErdosGallai.Scale.levelCycles line 92
  17. def OAI.ErdosGallai.Scale.levelPieces line 95
  18. lemma OAI.ErdosGallai.Scale.StageSplit.ledger line 98
  19. lemma OAI.ErdosGallai.Scale.level_ledger line 119
  20. def OAI.ErdosGallai.Scale.pastCycles line 130
  21. def OAI.ErdosGallai.Scale.pastPieces line 134
  22. lemma OAI.ErdosGallai.Scale.past_ledger line 138
  23. lemma OAI.ErdosGallai.Scale.past_partition line 148
  24. lemma OAI.ErdosGallai.Scale.levelCycles_good line 155
  25. lemma OAI.ErdosGallai.Scale.pastCycles_good line 161
  26. lemma OAI.ErdosGallai.Scale.levelPieces_subset line 171
  27. lemma OAI.ErdosGallai.Scale.levelPieces_mass line 178
  28. lemma OAI.ErdosGallai.Scale.levelCycles_length line 191
  29. lemma OAI.ErdosGallai.Scale.pastPieces_mass line 203
  30. lemma OAI.ErdosGallai.Scale.pastCycles_length line 210
  31. def OAI.ErdosGallai.Scale.CycleOrSingleEdge line 222
  32. def OAI.ErdosGallai.Scale.EdgeDecomposition line 227
  33. lemma OAI.ErdosGallai.Scale.cycleOrSingleEdge_subset line 236
  34. lemma OAI.ErdosGallai.Scale.cycleOrSingleEdge_map line 242
  35. lemma OAI.ErdosGallai.Scale.edgeDecomposition_of_indexed line 251
  36. theorem OAI.ErdosGallai.Scale.edgeDecomposition_singleEdges line 267
  37. theorem OAI.ErdosGallai.Scale.edgeDecomposition_assemble line 278
  38. def OAI.ErdosGallai.Scale.decompositionCost line 328
  39. lemma OAI.ErdosGallai.Scale.decompositionCost_spec line 331
  40. lemma OAI.ErdosGallai.Scale.decompositionCost_le line 334
  41. lemma OAI.ErdosGallai.Scale.decompositionCost_singleEdges line 337
  42. theorem OAI.ErdosGallai.Scale.edgeDecomposition_adjoin line 340
  43. lemma OAI.ErdosGallai.Scale.decompositionCost_adjoin line 395
  44. lemma OAI.ErdosGallai.Scale.edgeDecomposition_map line 416
  45. lemma OAI.ErdosGallai.Scale.decompositionCost_on line 425
  46. lemma OAI.ErdosGallai.Scale.edgeDecomposition_on line 441
  47. lemma OAI.ErdosGallai.Scale.decompositionCost_adjoin_same line 462
  48. lemma OAI.ErdosGallai.Scale.decompositionCost_assemble_same line 480
  49. lemma OAI.ErdosGallai.Scale.list_pairwise_get line 497
  50. lemma OAI.ErdosGallai.Scale.list_sum_get line 504
  51. lemma OAI.ErdosGallai.Scale.graphPartition_pairwise line 511
  52. lemma OAI.ErdosGallai.Scale.graphUnion_edges line 531
  53. lemma OAI.ErdosGallai.Scale.decompositionCost_partition line 545
  54. lemma OAI.ErdosGallai.Scale.decompositionCost_cycle line 553
  55. lemma OAI.ErdosGallai.Scale.decompositionCost_edgeCount line 565
  56. lemma OAI.ErdosGallai.Scale.decompositionCost_bot line 570
  57. lemma OAI.ErdosGallai.Scale.decompositionCost_partition_real line 575
  58. lemma OAI.ErdosGallai.Scale.decompositionCost_cycles line 582
  59. lemma OAI.ErdosGallai.Scale.partition_recombine line 589
  60. lemma OAI.ErdosGallai.Scale.cost_recombine line 598
  61. lemma OAI.ErdosGallai.Scale.graphUnion_le_of_members line 604
  62. lemma OAI.ErdosGallai.Scale.graphPartition_of_pairwise line 610