OAI/Combinatorics/ListHadwiger/WeightedBound.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ReedSeymour.mass line 13
  2. lemma OAI.ReedSeymour.mass_empty line 17
  3. lemma OAI.ReedSeymour.mass_univ line 18
  4. lemma OAI.ReedSeymour.mass_nonneg line 20
  5. lemma OAI.ReedSeymour.mass_mono line 24
  6. lemma OAI.ReedSeymour.mass_union line 34
  7. lemma OAI.ReedSeymour.mass_two_colors line 44
  8. lemma OAI.ReedSeymour.heavy_color line 54
  9. lemma OAI.ReedSeymour.independent_color_class line 61
  10. def OAI.ReedSeymour.Outside line 67
  11. structure OAI.ReedSeymour.EggCover line 69
  12. def OAI.ReedSeymour.EggCover.empty line 83
  13. lemma OAI.ReedSeymour.EggCover.outside_disjoint line 97
  14. structure OAI.ReedSeymour.Region line 101
  15. lemma OAI.ReedSeymour.EggCover.component_region line 106
  16. lemma OAI.ReedSeymour.ReachOn.stays line 112
  17. lemma OAI.ReedSeymour.Region.contains_connected line 122
  18. lemma OAI.ReedSeymour.Region.contains_of_touch line 129
  19. lemma OAI.ReedSeymour.outside_update_subset line 135
  20. def OAI.ReedSeymour.EggCover.replace line 147
  21. def OAI.ReedSeymour.EggCover.absorb line 223
  22. lemma OAI.ReedSeymour.outside_update_strict line 260
  23. lemma OAI.ReedSeymour.outside_update_ncard_lt line 270
  24. lemma OAI.ReedSeymour.EggCover.absorb_improves line 275
  25. def OAI.ReedSeymour.CliqueBound line 289
  26. lemma OAI.ReedSeymour.EggCover.free_color line 295
  27. lemma OAI.ReedSeymour.EggCover.add_improves line 345
  28. def OAI.ReedSeymour.Interface line 375
  29. lemma OAI.ReedSeymour.touch_iff_interface line 377
  30. lemma OAI.ReedSeymour.EggCover.improve_region line 380
  31. theorem OAI.ReedSeymour.exists_complete_egg_cover line 415
  32. lemma OAI.ReedSeymour.mass_iUnion line 428
  33. lemma OAI.ReedSeymour.EggCover.bag_mass line 453
  34. def OAI.ReedSeymour.EggCover.colorYolk line 464
  35. lemma OAI.ReedSeymour.EggCover.colorYolk_independent line 467
  36. lemma OAI.ReedSeymour.EggCover.colorYolk_mass line 478
  37. lemma OAI.ReedSeymour.EggCover.sum_yolk_mass line 491
  38. theorem OAI.ReedSeymour.dual_weight_bound line 498