OAI/Combinatorics/ListHadwiger/DistrictPaths.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LinearListHadwiger.exists_rotation_few_conflicts line 7
  2. lemma OAI.LinearListHadwiger.extend_from_ordinary line 37
  3. theorem OAI.LinearListHadwiger.ordinary_constrained_coloring_on line 175
  4. theorem OAI.LinearListHadwiger.colorable_of_connected_induced line 314
  5. lemma OAI.LinearListHadwiger.ordinary_chromatic_le_iff line 327
  6. theorem OAI.LinearListHadwiger.ordinary_connectivity_extraction line 335
  7. structure OAI.LinearListHadwiger.WeavingWithin line 358
  8. def OAI.LinearListHadwiger.WovenOn line 369
  9. def OAI.LinearListHadwiger.Woven line 376
  10. structure OAI.LinearListHadwiger.DistrictVisits line 379
  11. lemma OAI.LinearListHadwiger.first_district_visit line 392
  12. lemma OAI.LinearListHadwiger.district_visits_exist line 419
  13. lemma OAI.LinearListHadwiger.DistrictVisits.initial_subset line 434
  14. lemma OAI.LinearListHadwiger.DistrictVisits.terminal_subset line 437
  15. lemma OAI.LinearListHadwiger.DistrictVisits.entry_on line 440
  16. lemma OAI.LinearListHadwiger.DistrictVisits.exit_on line 442
  17. theorem OAI.LinearListHadwiger.reroute_woven_district line 446