OAI/Combinatorics/ListHadwiger/TerminalGrouping.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.Knitting.density line 10
  2. lemma OAI.LinearListHadwiger.Knitting.model_card_le line 13
  3. def OAI.LinearListHadwiger.Knitting.model_singletons line 23
  4. def OAI.LinearListHadwiger.Knitting.model_relabel line 31
  5. lemma OAI.LinearListHadwiger.Knitting.density_iso line 39
  6. theorem OAI.LinearListHadwiger.Knitting.maximal_minor_density line 44
  7. def OAI.LinearListHadwiger.Knitting.contractEdge line 65
  8. def OAI.LinearListHadwiger.Knitting.contract_model line 77
  9. def OAI.LinearListHadwiger.Knitting.common line 117
  10. def OAI.LinearListHadwiger.Knitting.edgeGood line 120
  11. def OAI.LinearListHadwiger.Knitting.proj line 123
  12. lemma OAI.LinearListHadwiger.Knitting.proj_collision line 126
  13. lemma OAI.LinearListHadwiger.Knitting.proj_adj line 155
  14. theorem OAI.LinearListHadwiger.Knitting.contract_edge_count line 176
  15. lemma OAI.LinearListHadwiger.Knitting.density_mul_order line 246
  16. lemma OAI.LinearListHadwiger.Knitting.density_nonneg line 251
  17. lemma OAI.LinearListHadwiger.Knitting.degree_le_twice_density line 254
  18. lemma OAI.LinearListHadwiger.Knitting.common_of_max_density line 268
  19. def OAI.LinearListHadwiger.Knitting.model_induce line 287
  20. lemma OAI.LinearListHadwiger.Knitting.neighborhood_degree line 296
  21. lemma OAI.LinearListHadwiger.Knitting.kConnected_iso line 312
  22. theorem OAI.LinearListHadwiger.Knitting.small_minor_core line 337
  23. lemma OAI.LinearListHadwiger.Knitting.kConnected_mono line 445
  24. lemma OAI.LinearListHadwiger.Knitting.kConnected_restrict line 449
  25. lemma OAI.LinearListHadwiger.Knitting.density_of_connectivity line 462
  26. lemma OAI.LinearListHadwiger.Knitting.bags_meeting_bound line 479
  27. theorem OAI.LinearListHadwiger.Knitting.group_terminals line 498