OAI/Combinatorics/ListHadwiger/District.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.District.Statement line 11
  2. def OAI.LinearListHadwiger.District.outside line 17
  3. lemma OAI.LinearListHadwiger.District.mem_outside line 20
  4. lemma OAI.LinearListHadwiger.District.outside_disjoint line 23
  5. lemma OAI.LinearListHadwiger.District.degree_sum_comm line 26
  6. lemma OAI.LinearListHadwiger.District.degree_sum_split line 36
  7. def OAI.LinearListHadwiger.District.loss2 line 61
  8. lemma OAI.LinearListHadwiger.District.outside_pos line 64
  9. lemma OAI.LinearListHadwiger.District.darts_sum line 69
  10. lemma OAI.LinearListHadwiger.District.loss2_identity line 75
  11. theorem OAI.LinearListHadwiger.District.restricted_degree_loss line 95
  12. lemma OAI.LinearListHadwiger.District.outside_insert line 112
  13. lemma OAI.LinearListHadwiger.District.neighborhood_increment line 125
  14. lemma OAI.LinearListHadwiger.District.loss2_insert line 144
  15. lemma OAI.LinearListHadwiger.District.loss2_singleton line 161
  16. theorem OAI.LinearListHadwiger.District.surviving_core line 178
  17. lemma OAI.LinearListHadwiger.District.outside_card_le line 239
  18. theorem OAI.LinearListHadwiger.District.cheap_neighborhood line 247
  19. abbrev OAI.LinearListHadwiger.District.ContractVertex line 356
  20. def OAI.LinearListHadwiger.District.contractSet line 358
  21. def OAI.LinearListHadwiger.District.contractSet_model line 372
  22. lemma OAI.LinearListHadwiger.District.contract_card line 404
  23. lemma OAI.LinearListHadwiger.District.contract_root_degree line 408
  24. lemma OAI.LinearListHadwiger.District.contract_remaining_darts line 425
  25. lemma OAI.LinearListHadwiger.District.contract_darts line 448
  26. lemma OAI.LinearListHadwiger.District.degree_partition line 453
  27. lemma OAI.LinearListHadwiger.District.darts_partition line 463
  28. theorem OAI.LinearListHadwiger.District.loss2_contract line 477
  29. lemma OAI.LinearListHadwiger.District.expand_card line 484
  30. structure OAI.LinearListHadwiger.District.CheapMinor line 496
  31. def OAI.LinearListHadwiger.District.CheapMinor.initial line 506
  32. lemma OAI.LinearListHadwiger.District.CheapMinor.exists_minimum line 516
  33. def OAI.LinearListHadwiger.District.CheapMinor.big line 523
  34. lemma OAI.LinearListHadwiger.District.CheapMinor.small line 526
  35. lemma OAI.LinearListHadwiger.District.CheapMinor.big_card line 531
  36. def OAI.LinearListHadwiger.District.CheapMinor.contract line 542
  37. theorem OAI.LinearListHadwiger.District.CheapMinor.no_cheap line 577
  38. lemma OAI.LinearListHadwiger.District.kConnected_image line 592
  39. lemma OAI.LinearListHadwiger.District.CheapMinor.lift_small line 623
  40. def OAI.LinearListHadwiger.District.badY line 644
  41. def OAI.LinearListHadwiger.District.badZ line 646
  42. def OAI.LinearListHadwiger.District.badSet line 648
  43. lemma OAI.LinearListHadwiger.District.bad_size line 651
  44. lemma OAI.LinearListHadwiger.District.bad_degree_sum line 702
  45. theorem OAI.LinearListHadwiger.District.bad_set_core line 742
  46. theorem OAI.LinearListHadwiger.District.district_finite line 789
  47. lemma OAI.LinearListHadwiger.District.darts_induce line 850
  48. lemma OAI.LinearListHadwiger.District.coarse_darts line 857
  49. lemma OAI.LinearListHadwiger.District.district_cutoff line 886
  50. lemma OAI.LinearListHadwiger.District.district_order line 894
  51. theorem OAI.LinearListHadwiger.District.district line 912