OAI/Combinatorics/ThinTrees/BasePacking.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.StrongThinTree.Packing.span line 16
  2. lemma OAI.StrongThinTree.Packing.span_mono line 20
  3. lemma OAI.StrongThinTree.Packing.span_insert line 24
  4. lemma OAI.StrongThinTree.Packing.mem_span_self line 29
  5. lemma OAI.StrongThinTree.Packing.span_le_iff line 33
  6. lemma OAI.StrongThinTree.Packing.indep_rank line 41
  7. lemma OAI.StrongThinTree.Packing.support_exchange line 52
  8. def OAI.StrongThinTree.Packing.Valid line 70
  9. abbrev OAI.StrongThinTree.Packing.State line 73
  10. def OAI.StrongThinTree.Packing.cost line 75
  11. def OAI.StrongThinTree.Packing.unused line 77
  12. lemma OAI.StrongThinTree.Packing.valid_empty line 80
  13. lemma OAI.StrongThinTree.Packing.valid_update line 86
  14. lemma OAI.StrongThinTree.Packing.disjoint_insert_unused line 104
  15. lemma OAI.StrongThinTree.Packing.cost_update line 112
  16. lemma OAI.StrongThinTree.Packing.exists_maximal_state line 134
  17. lemma OAI.StrongThinTree.Packing.maximal_unused_mem_span line 144
  18. def OAI.StrongThinTree.Packing.Move line 156
  19. lemma OAI.StrongThinTree.Packing.unused_after_exchange line 161
  20. lemma OAI.StrongThinTree.Packing.Move.cost_eq line 174
  21. lemma OAI.StrongThinTree.Packing.reachable_cost_eq line 185
  22. lemma OAI.StrongThinTree.Packing.reachable_maximal line 192
  23. def OAI.StrongThinTree.Packing.recycled line 199
  24. lemma OAI.StrongThinTree.Packing.mem_recycled line 204
  25. lemma OAI.StrongThinTree.Packing.unused_span_recycled line 210
  26. lemma OAI.StrongThinTree.Packing.move_span_recycled_eq line 233
  27. lemma OAI.StrongThinTree.Packing.reachable_span_recycled_eq line 265
  28. lemma OAI.StrongThinTree.Packing.span_recycled_eq line 275
  29. lemma OAI.StrongThinTree.Packing.cost_decomposition line 287
  30. theorem OAI.StrongThinTree.Packing.vector_base_packing line 324
  31. lemma OAI.StrongThinTree.Packing.masked_span line 350
  32. theorem OAI.StrongThinTree.Packing.vector_base_packing_on line 365
  33. abbrev OAI.StrongThinTree.MultiGraph.edgeSpan line 403
  34. def OAI.StrongThinTree.MultiGraph.Same line 405
  35. lemma OAI.StrongThinTree.MultiGraph.same_refl line 408
  36. lemma OAI.StrongThinTree.MultiGraph.same_symm line 411
  37. lemma OAI.StrongThinTree.MultiGraph.same_trans line 415
  38. def OAI.StrongThinTree.MultiGraph.components line 420
  39. def OAI.StrongThinTree.MultiGraph.rep line 424
  40. lemma OAI.StrongThinTree.MultiGraph.rep_same line 426
  41. lemma OAI.StrongThinTree.MultiGraph.rep_eq_iff line 429
  42. lemma OAI.StrongThinTree.MultiGraph.rep_idempotent line 436
  43. lemma OAI.StrongThinTree.MultiGraph.same_endpoints line 439
  44. lemma OAI.StrongThinTree.MultiGraph.rep_endpoints line 442
  45. abbrev OAI.StrongThinTree.MultiGraph.repDifference line 446
  46. lemma OAI.StrongThinTree.MultiGraph.repDifference_mem line 449
  47. lemma OAI.StrongThinTree.MultiGraph.repDifference_independent line 452
  48. lemma OAI.StrongThinTree.MultiGraph.edgeSpan_eq_repSpan line 466
  49. def OAI.StrongThinTree.MultiGraph.componentCount line 488
  50. theorem OAI.StrongThinTree.MultiGraph.incidence_rank line 490
  51. lemma OAI.StrongThinTree.MultiGraph.sumOn_point line 505
  52. theorem OAI.StrongThinTree.MultiGraph.connected_iff_same line 510
  53. lemma OAI.StrongThinTree.MultiGraph.connected_of_span_eq line 564
  54. theorem OAI.StrongThinTree.MultiGraph.spanningTree_iff_independent line 572
  55. lemma OAI.StrongThinTree.MultiGraph.componentCount_pos line 594
  56. lemma OAI.StrongThinTree.MultiGraph.componentCount_le line 598
  57. lemma OAI.StrongThinTree.MultiGraph.connected_componentCount line 601
  58. lemma OAI.StrongThinTree.MultiGraph.connected_rank line 616
  59. lemma OAI.StrongThinTree.MultiGraph.spanningTree_card line 620
  60. def OAI.StrongThinTree.MultiGraph.crossing line 624
  61. def OAI.StrongThinTree.MultiGraph.partitionSize line 627
  62. def OAI.StrongThinTree.MultiGraph.TreePackable line 629
  63. lemma OAI.StrongThinTree.MultiGraph.connected_of_componentCount_eq_one line 633
  64. lemma OAI.StrongThinTree.MultiGraph.crossing_components_subset line 645
  65. lemma OAI.StrongThinTree.MultiGraph.crossing_components_self line 651
  66. theorem OAI.StrongThinTree.MultiGraph.partition_criterion_sufficient line 657
  67. lemma OAI.StrongThinTree.MultiGraph.sum_partition_cuts line 687
  68. lemma OAI.StrongThinTree.MultiGraph.partition_fiber_proper line 711
  69. theorem OAI.StrongThinTree.MultiGraph.edgeConnected_treePackable line 722
  70. lemma OAI.StrongThinTree.MultiGraph.same_preserves_label line 742
  71. lemma OAI.StrongThinTree.MultiGraph.partitionSize_le_components line 764
  72. lemma OAI.StrongThinTree.MultiGraph.spanningTree_crossing line 773
  73. theorem OAI.StrongThinTree.MultiGraph.partition_criterion_necessary line 794