OAI/Combinatorics/ListHadwiger/Exchanges.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.BagRouting.used line 12
  2. def OAI.LinearListHadwiger.BagRouting.Minimal line 15
  3. lemma OAI.LinearListHadwiger.BagRouting.exists_minimal line 18
  4. def OAI.LinearListHadwiger.BagRouting.replace line 29
  5. lemma OAI.LinearListHadwiger.BagRouting.replace_shorter line 64
  6. lemma OAI.LinearListHadwiger.BagRouting.Minimal.walk_length_le line 83
  7. lemma OAI.LinearListHadwiger.BagRouting.Minimal.no_long_shortcut line 99
  8. lemma OAI.LinearListHadwiger.BagRouting.Minimal.path_neighbors_le_three line 132
  9. def OAI.LinearListHadwiger.BagRouting.usedFinset line 167
  10. lemma OAI.LinearListHadwiger.BagRouting.mem_usedFinset line 170
  11. lemma OAI.LinearListHadwiger.BagRouting.Minimal.used_neighbors_le line 174
  12. lemma OAI.LinearListHadwiger.BagRouting.mem_take_indices line 194
  13. lemma OAI.LinearListHadwiger.BagRouting.mem_drop_indices line 204
  14. lemma OAI.LinearListHadwiger.BagRouting.take_drop_disjoint line 212
  15. lemma OAI.LinearListHadwiger.BagRouting.source_not_mem_drop line 222
  16. structure OAI.LinearListHadwiger.BagRouting.Exchange line 230
  17. def OAI.LinearListHadwiger.BagRouting.Exchange.front line 244
  18. def OAI.LinearListHadwiger.BagRouting.Exchange.tail line 248
  19. lemma OAI.LinearListHadwiger.BagRouting.Exchange.front_subset line 251
  20. lemma OAI.LinearListHadwiger.BagRouting.Exchange.tail_subset line 261
  21. lemma OAI.LinearListHadwiger.BagRouting.Exchange.not_source_tail line 271
  22. lemma OAI.LinearListHadwiger.BagRouting.Exchange.front_tail_disjoint line 279
  23. def OAI.LinearListHadwiger.BagRouting.Exchange.walk line 287
  24. lemma OAI.LinearListHadwiger.BagRouting.Exchange.walk_support line 292
  25. lemma OAI.LinearListHadwiger.BagRouting.Exchange.support_overlap line 306
  26. def OAI.LinearListHadwiger.BagRouting.Exchange.routing line 325
  27. lemma OAI.LinearListHadwiger.BagRouting.Exchange.length_inequality line 354
  28. lemma OAI.LinearListHadwiger.BagRouting.Exchange.shorter line 377
  29. lemma OAI.LinearListHadwiger.BagRouting.Minimal.no_exchange line 404
  30. lemma OAI.LinearListHadwiger.BagRouting.cycle_permutation line 409
  31. lemma OAI.LinearListHadwiger.BagRouting.Minimal.low_degree line 445