OAI/Combinatorics/ListHadwiger/Basic.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LinearListHadwiger.choosable_mono line 7
  2. theorem OAI.LinearListHadwiger.choosable_card line 12
  3. theorem OAI.LinearListHadwiger.choosable_listChromaticNumber line 27
  4. theorem OAI.LinearListHadwiger.listChromaticNumber_le_iff line 32
  5. theorem OAI.LinearListHadwiger.listChromaticNumber_le_card line 39
  6. theorem OAI.LinearListHadwiger.cliqueMinor_order_le_card line 43
  7. theorem OAI.LinearListHadwiger.cliqueMinor_zero line 59
  8. theorem OAI.LinearListHadwiger.hadwiger_bddAbove line 65
  9. theorem OAI.LinearListHadwiger.cliqueMinor_le_hadwigerNumber line 69
  10. theorem OAI.LinearListHadwiger.hasCliqueMinor_hadwigerNumber line 73
  11. theorem OAI.LinearListHadwiger.cliqueMinor_one line 77
  12. theorem OAI.LinearListHadwiger.one_le_hadwigerNumber line 89
  13. def OAI.LinearListHadwiger.KConnectedOn line 93
  14. structure OAI.LinearListHadwiger.SeparatorSplit line 97
  15. lemma OAI.LinearListHadwiger.exists_separator line 107
  16. lemma OAI.LinearListHadwiger.choosable_induce line 156
  17. def OAI.LinearListHadwiger.ProperOn line 183
  18. def OAI.LinearListHadwiger.ValidOn line 187
  19. lemma OAI.LinearListHadwiger.ValidOn.mono line 191
  20. lemma OAI.LinearListHadwiger.extend_from_choosable line 196
  21. def OAI.LinearListHadwiger.vertexCost line 249
  22. def OAI.LinearListHadwiger.constraintCost line 253
  23. lemma OAI.LinearListHadwiger.constraintCost_eq line 257
  24. lemma OAI.LinearListHadwiger.constraintCost_card_bound line 272
  25. lemma OAI.LinearListHadwiger.constraintCost_mono line 282
  26. lemma OAI.LinearListHadwiger.promote_constraints line 287
  27. lemma OAI.LinearListHadwiger.choosable_of_iso line 337
  28. lemma OAI.LinearListHadwiger.choosable_of_embedding line 347
  29. lemma OAI.LinearListHadwiger.choosable_induce_subset line 351