OAI/Combinatorics/ListHadwiger/Separators.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LinearListHadwiger.SeparatorSplit.swap line 11
  2. lemma OAI.LinearListHadwiger.SeparatorSplit.left_union_subset line 18
  3. lemma OAI.LinearListHadwiger.SeparatorSplit.right_subset line 22
  4. lemma OAI.LinearListHadwiger.SeparatorSplit.left_union_disjoint line 26
  5. lemma OAI.LinearListHadwiger.SeparatorSplit.sum_eq line 29
  6. lemma OAI.LinearListHadwiger.SeparatorSplit.left_union_ssubset line 33
  7. lemma OAI.LinearListHadwiger.constraintCost_restrict line 41
  8. lemma OAI.LinearListHadwiger.precolor_cost_le line 48
  9. lemma OAI.LinearListHadwiger.exists_balanced_separator line 54
  10. def OAI.LinearListHadwiger.extraForbidden line 68
  11. lemma OAI.LinearListHadwiger.extraForbidden_subset line 73
  12. lemma OAI.LinearListHadwiger.extraForbidden_cost line 79
  13. lemma OAI.LinearListHadwiger.first_side_cost line 101
  14. lemma OAI.LinearListHadwiger.second_side_cost line 123
  15. lemma OAI.LinearListHadwiger.SeparatorSplit.glue line 143
  16. lemma OAI.LinearListHadwiger.separator_precolor line 193
  17. theorem OAI.LinearListHadwiger.constrained_coloring_on line 225
  18. theorem OAI.LinearListHadwiger.choosable_of_connected_induced line 365
  19. theorem OAI.LinearListHadwiger.list_connectivity_extraction line 385
  20. lemma OAI.LinearListHadwiger.connected_induce_star line 406
  21. theorem OAI.LinearListHadwiger.cliqueMinor_of_subdivision line 417
  22. lemma OAI.LinearListHadwiger.cliqueMinor_of_saturated_pairs line 453
  23. def OAI.LinearListHadwiger.neighborPairs line 494
  24. lemma OAI.LinearListHadwiger.mem_neighborPairs line 499