OAI/Combinatorics/ListHadwiger/MinorModels.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.MinorModel.expand line 11
  2. lemma OAI.LinearListHadwiger.MinorModel.branch_subset_expand line 14
  3. lemma OAI.LinearListHadwiger.MinorModel.expand_connected line 17
  4. lemma OAI.LinearListHadwiger.MinorModel.expand_disjoint line 50
  5. theorem OAI.LinearListHadwiger.MinorModel.lift_clique line 58
  6. theorem OAI.LinearListHadwiger.MinorModel.hadwiger_le line 68
  7. structure OAI.LinearListHadwiger.BagRouting line 74
  8. def OAI.LinearListHadwiger.BagRouting.totalLength line 87
  9. def OAI.LinearListHadwiger.BagRouting.truncate line 90
  10. lemma OAI.LinearListHadwiger.BagRouting.truncate_length_lt line 126
  11. theorem OAI.LinearListHadwiger.BagRouting.exists_avoiding_unused line 159
  12. theorem OAI.LinearListHadwiger.bagRouting_of_double_packing line 177
  13. lemma OAI.LinearListHadwiger.exists_region_avoiding line 220
  14. structure OAI.LinearListHadwiger.RootedCliqueModel line 242
  15. theorem OAI.LinearListHadwiger.rootedModel_of_packing line 249