OAI/Combinatorics/ThinTrees/PartitionRank.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrongThinTree.MultiGraph.internal line 14
  2. def OAI.StrongThinTree.MultiGraph.ConnectedOn line 17
  3. def OAI.StrongThinTree.MultiGraph.TreeOn line 20
  4. def OAI.StrongThinTree.MultiGraph.PackableOn line 23
  5. lemma OAI.StrongThinTree.MultiGraph.connectedOn_mono_span line 28
  6. lemma OAI.StrongThinTree.MultiGraph.connectedOn_mono line 33
  7. lemma OAI.StrongThinTree.MultiGraph.independent_spanning_subset line 37
  8. lemma OAI.StrongThinTree.MultiGraph.packableOn_iff_trees line 49
  9. lemma OAI.StrongThinTree.MultiGraph.packableOn_singleton line 68
  10. lemma OAI.StrongThinTree.MultiGraph.packableOn_mono_edges line 76
  11. lemma OAI.StrongThinTree.MultiGraph.splice_span line 81
  12. theorem OAI.StrongThinTree.MultiGraph.packableOn_union line 90
  13. def OAI.StrongThinTree.MultiGraph.MaxPackable line 125
  14. def OAI.StrongThinTree.MultiGraph.packingParts line 129
  15. lemma OAI.StrongThinTree.MultiGraph.exists_maxPackable line 132
  16. lemma OAI.StrongThinTree.MultiGraph.maxPackable_disjoint line 145
  17. lemma OAI.StrongThinTree.MultiGraph.maxPackable_contains line 154
  18. theorem OAI.StrongThinTree.MultiGraph.packingParts_partition line 159
  19. theorem OAI.StrongThinTree.MultiGraph.packingParts_coarsens line 174
  20. lemma OAI.StrongThinTree.MultiGraph.connectedOn_univ line 182
  21. lemma OAI.StrongThinTree.MultiGraph.packableOn_univ line 186
  22. def OAI.StrongThinTree.MultiGraph.vertexProjection line 200
  23. lemma OAI.StrongThinTree.MultiGraph.vertexProjection_point line 205
  24. lemma OAI.StrongThinTree.MultiGraph.restrict_span line 211
  25. lemma OAI.StrongThinTree.MultiGraph.restrict_same line 227
  26. theorem OAI.StrongThinTree.Packing.packing_certificate_on line 245
  27. lemma OAI.StrongThinTree.MultiGraph.component_packable_of_certificate line 294
  28. def OAI.StrongThinTree.MultiGraph.partOf line 315
  29. lemma OAI.StrongThinTree.MultiGraph.partOf_spec line 318
  30. lemma OAI.StrongThinTree.MultiGraph.partOf_eq_iff line 323
  31. lemma OAI.StrongThinTree.MultiGraph.partOf_eq_of_mem line 332
  32. def OAI.StrongThinTree.MultiGraph.partLabel line 338
  33. lemma OAI.StrongThinTree.MultiGraph.partLabel_mem line 341
  34. lemma OAI.StrongThinTree.MultiGraph.partLabel_eq_iff line 344
  35. lemma OAI.StrongThinTree.MultiGraph.partLabel_idempotent line 355
  36. lemma OAI.StrongThinTree.MultiGraph.partLabel_size line 360
  37. lemma OAI.StrongThinTree.Packing.span_rank_le_card line 388
  38. lemma OAI.StrongThinTree.Packing.rank_le_sdiff_card_add line 396
  39. def OAI.StrongThinTree.MultiGraph.withinParts line 418
  40. lemma OAI.StrongThinTree.MultiGraph.internal_subset_withinParts line 421
  41. lemma OAI.StrongThinTree.MultiGraph.same_withinParts line 428
  42. lemma OAI.StrongThinTree.MultiGraph.componentCount_eq_partitionSize line 445
  43. lemma OAI.StrongThinTree.MultiGraph.withinParts_rank line 460
  44. lemma OAI.StrongThinTree.MultiGraph.withinParts_spanning_packing line 465
  45. lemma OAI.StrongThinTree.MultiGraph.recycled_subset_withinParts line 507
  46. lemma OAI.StrongThinTree.MultiGraph.not_packable_of_parts line 529
  47. lemma OAI.StrongThinTree.MultiGraph.forest_card_le line 542
  48. lemma OAI.StrongThinTree.MultiGraph.packing_cost_lt line 550
  49. lemma OAI.StrongThinTree.MultiGraph.withinParts_rank_count line 575
  50. theorem OAI.StrongThinTree.MultiGraph.packingParts_crossing_lt line 596