OAI/Combinatorics/ListHadwiger/Separability.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.Fractional.cliqueBlowup line 9
  2. lemma OAI.LinearListHadwiger.Fractional.stable_blowup_projection line 18
  3. lemma OAI.LinearListHadwiger.Fractional.stable_blowup_injOn line 26
  4. lemma OAI.LinearListHadwiger.Fractional.Dual.blowup line 33
  5. lemma OAI.LinearListHadwiger.Fractional.dual_sum_le_colors line 42
  6. lemma OAI.LinearListHadwiger.Fractional.number_le_colorable line 56
  7. theorem OAI.LinearListHadwiger.Fractional.cliqueBlowup_chromatic_lower line 63
  8. lemma OAI.LinearListHadwiger.Fractional.cliqueBlowup_colorable_rounded line 73
  9. theorem OAI.LinearListHadwiger.Fractional.cliqueBlowup_chromatic_upper line 133
  10. inductive OAI.LinearListHadwiger.FixedDecomposition.Tree line 160
  11. theorem OAI.LinearListHadwiger.FixedDecomposition.exists_tree line 165
  12. def OAI.LinearListHadwiger.FixedDecomposition.Tree.leaves line 176
  13. def OAI.LinearListHadwiger.FixedDecomposition.Tree.separators line 180
  14. def OAI.LinearListHadwiger.FixedDecomposition.budget line 184
  15. lemma OAI.LinearListHadwiger.FixedDecomposition.budget_branch line 186
  16. lemma OAI.LinearListHadwiger.FixedDecomposition.Tree.leaf_subset line 205
  17. lemma OAI.LinearListHadwiger.FixedDecomposition.Tree.separator_subset line 216
  18. lemma OAI.LinearListHadwiger.FixedDecomposition.Tree.leaf_stop line 227
  19. lemma OAI.LinearListHadwiger.FixedDecomposition.Tree.separator_small line 238
  20. theorem OAI.LinearListHadwiger.FixedDecomposition.exists_bounded_tree line 249
  21. lemma OAI.LinearListHadwiger.FixedDecomposition.budget_le_square line 279
  22. lemma OAI.LinearListHadwiger.FixedDecomposition.reachable_preserves line 286
  23. lemma OAI.LinearListHadwiger.FixedDecomposition.confine_split line 294
  24. lemma OAI.LinearListHadwiger.FixedDecomposition.Tree.confine line 337
  25. lemma OAI.LinearListHadwiger.FixedDecomposition.card_finset_subtype_le line 360
  26. lemma OAI.LinearListHadwiger.FixedDecomposition.lifted_separator_card line 366
  27. lemma OAI.LinearListHadwiger.FixedDecomposition.cliqueBlowup_leaf_hom line 385
  28. theorem OAI.LinearListHadwiger.FixedDecomposition.fractional_le_leaves_add_separator line 404