OAI/Combinatorics/ListHadwiger/RecursiveDistricts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.Recursion.child line 9
  2. def OAI.LinearListHadwiger.Recursion.triBlock line 11
  3. def OAI.LinearListHadwiger.Recursion.district line 13
  4. def OAI.LinearListHadwiger.Recursion.districtLabels line 15
  5. lemma OAI.LinearListHadwiger.Recursion.district_labels_card line 18
  6. lemma OAI.LinearListHadwiger.Recursion.district_mem_labels line 39
  7. lemma OAI.LinearListHadwiger.Recursion.district_pair_coverage line 43
  8. lemma OAI.LinearListHadwiger.Recursion.district_same_injective line 51
  9. lemma OAI.LinearListHadwiger.Recursion.child_shrink line 58
  10. lemma OAI.LinearListHadwiger.Recursion.path_capacity line 62
  11. lemma OAI.LinearListHadwiger.Recursion.district_indices line 66
  12. theorem OAI.LinearListHadwiger.Recursion.three_district_model line 89
  13. theorem OAI.LinearListHadwiger.Recursion.separability_on line 191
  14. theorem OAI.LinearListHadwiger.Recursion.three_regions line 222