OAI/Combinatorics/ListHadwiger/BagContraction.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.BagContraction.Remnant line 12
  2. abbrev OAI.LinearListHadwiger.BagContraction.Vertex line 13
  3. def OAI.LinearListHadwiger.BagContraction.branch line 15
  4. def OAI.LinearListHadwiger.BagContraction.graph line 19
  5. instance OAI.LinearListHadwiger.BagContraction.(instance at line 26) line 26
  6. lemma OAI.LinearListHadwiger.BagContraction.branch_disjoint line 30
  7. def OAI.LinearListHadwiger.BagContraction.model line 45
  8. def OAI.LinearListHadwiger.BagContraction.liftSet line 58
  9. lemma OAI.LinearListHadwiger.BagContraction.liftSet_connected line 61
  10. lemma OAI.LinearListHadwiger.BagContraction.liftSet_disjoint line 81
  11. lemma OAI.LinearListHadwiger.BagContraction.liftSet_adj_target line 89
  12. def OAI.LinearListHadwiger.BagRouting.region line 100
  13. lemma OAI.LinearListHadwiger.BagRouting.region_connected line 104
  14. lemma OAI.LinearListHadwiger.BagRouting.root_mem_region line 111
  15. lemma OAI.LinearListHadwiger.BagRouting.region_congestion line 115
  16. lemma OAI.LinearListHadwiger.BagRouting.region_avoids_unused line 158
  17. theorem OAI.LinearListHadwiger.packing_from_regions line 173
  18. def OAI.LinearListHadwiger.RootedCliqueModel.reindex line 205
  19. theorem OAI.LinearListHadwiger.rooting_from_eligible line 214
  20. lemma OAI.LinearListHadwiger.eligible_bags_card line 304
  21. theorem OAI.LinearListHadwiger.rooting line 334