OAI/Combinatorics/CycleDecomposition/Templates.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ErdosGallai.Batch.demandLoad line 18
  2. theorem OAI.ErdosGallai.Batch.demand_load_le_degree line 21
  3. lemma OAI.ErdosGallai.Batch.start_has_incident_edge line 56
  4. lemma OAI.ErdosGallai.Batch.finish_has_incident_edge line 61
  5. theorem OAI.ErdosGallai.Batch.path_demands_load_le_degree line 68
  6. lemma OAI.ErdosGallai.Batch.disjoint_sum_blocks line 81
  7. def OAI.ErdosGallai.Batch.CycleOrSingleEdge line 102
  8. def OAI.ErdosGallai.Batch.EdgeDecomposition line 107
  9. lemma OAI.ErdosGallai.Batch.cycleOrSingleEdge_subset line 116
  10. lemma OAI.ErdosGallai.Batch.cycleOrSingleEdge_map line 122
  11. lemma OAI.ErdosGallai.Batch.edgeDecomposition_of_indexed line 131
  12. theorem OAI.ErdosGallai.Batch.edgeDecomposition_singleEdges line 147
  13. theorem OAI.ErdosGallai.Batch.edgeDecomposition_assemble line 158
  14. def OAI.ErdosGallai.Batch.decompositionCost line 208
  15. lemma OAI.ErdosGallai.Batch.decompositionCost_spec line 211
  16. lemma OAI.ErdosGallai.Batch.decompositionCost_le line 214
  17. lemma OAI.ErdosGallai.Batch.decompositionCost_singleEdges line 217
  18. theorem OAI.ErdosGallai.Batch.edgeDecomposition_adjoin line 220
  19. lemma OAI.ErdosGallai.Batch.decompositionCost_adjoin line 275
  20. lemma OAI.ErdosGallai.Batch.edgeDecomposition_map line 296
  21. lemma OAI.ErdosGallai.Batch.decompositionCost_on line 305
  22. lemma OAI.ErdosGallai.Batch.edgeDecomposition_on line 321
  23. lemma OAI.ErdosGallai.Batch.endpointLoad_subtype_le line 343
  24. theorem OAI.ErdosGallai.Batch.uniform_multi_batch_routing line 352
  25. structure OAI.ErdosGallai.Batch.CycleOutline line 417
  26. def OAI.ErdosGallai.Batch.CycleOutline.edges line 436
  27. def OAI.ErdosGallai.Batch.CycleOutline.vertices line 437
  28. abbrev OAI.ErdosGallai.Batch.CycleOutline.Switch line 438
  29. instance OAI.ErdosGallai.Batch.CycleOutline.(instance at line 439) line 439
  30. lemma OAI.ErdosGallai.Batch.CycleOutline.edges_subset line 441
  31. lemma OAI.ErdosGallai.Batch.CycleOutline.fst_mem line 444
  32. lemma OAI.ErdosGallai.Batch.CycleOutline.snd_mem line 448
  33. lemma OAI.ErdosGallai.Batch.CycleOutline.outgoing line 454
  34. lemma OAI.ErdosGallai.Batch.CycleOutline.incoming line 460
  35. lemma OAI.ErdosGallai.Batch.CycleOutline.endpoint_incident line 468
  36. lemma OAI.ErdosGallai.Batch.CycleOutline.endpoint_unique line 485
  37. lemma OAI.ErdosGallai.Batch.CycleOutline.vertices_card_support line 495
  38. lemma OAI.ErdosGallai.Batch.CycleOutline.vertices_card line 510
  39. lemma OAI.ErdosGallai.Batch.CycleOutline.mem_vertices line 513
  40. theorem OAI.ErdosGallai.Batch.CycleOutline.complete line 516
  41. structure OAI.ErdosGallai.Batch.RoutingTemplate line 592
  42. def OAI.ErdosGallai.Batch.RoutingTemplate.ofCycle line 613
  43. def OAI.ErdosGallai.Batch.RoutingTemplate.ofSingle line 629
  44. def OAI.ErdosGallai.Batch.RoutingTemplate.ofPath line 642
  45. lemma OAI.ErdosGallai.Batch.RoutingTemplate.ofCycle_arity_card line 672
  46. lemma OAI.ErdosGallai.Batch.RoutingTemplate.ofPath_vertices_card line 675
  47. theorem OAI.ErdosGallai.Batch.uniform_resolve_templates line 680