OAI/Combinatorics/CycleDecomposition/CycleLifting.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ErdosGallai.Batch.routing_length_upper line 17
  2. lemma OAI.ErdosGallai.Batch.eventually_logb_le_power line 41
  3. lemma OAI.ErdosGallai.Batch.eventually_constant_le_power line 50
  4. lemma OAI.ErdosGallai.Batch.eventually_const_mul_power_le line 54
  5. theorem OAI.ErdosGallai.Batch.eventually_routing_length line 62
  6. theorem OAI.ErdosGallai.Batch.batch_routing_margin line 95
  7. lemma OAI.ErdosGallai.Batch.eventually_reservoir_capacity line 134
  8. theorem OAI.ErdosGallai.Batch.residue_routing_margin line 152
  9. def OAI.ErdosGallai.Batch.CutExpansionOn line 196
  10. lemma OAI.ErdosGallai.Batch.subtype_image_compl line 200
  11. lemma OAI.ErdosGallai.Batch.induced_interedges_card line 214
  12. lemma OAI.ErdosGallai.Batch.cutExpansion_induce line 239
  13. lemma OAI.ErdosGallai.Batch.pathInterior_map line 256
  14. theorem OAI.ErdosGallai.Batch.team_routing_on_set line 268
  15. theorem OAI.ErdosGallai.Batch.uniform_batch_routing line 339
  16. structure OAI.ErdosGallai.Batch.CycleVisit line 377
  17. inductive OAI.ErdosGallai.Batch.VisitChain line 382
  18. def OAI.ErdosGallai.Batch.VisitChain.walk line 391
  19. def OAI.ErdosGallai.Batch.VisitChain.visits line 395
  20. def OAI.ErdosGallai.Batch.VisitChain.links line 399
  21. def OAI.ErdosGallai.Batch.VisitChain.switchEdges line 403
  22. lemma OAI.ErdosGallai.Batch.VisitChain.mem_support_iff line 406
  23. lemma OAI.ErdosGallai.Batch.VisitChain.isPath_of_separated line 422
  24. lemma OAI.ErdosGallai.Batch.VisitChain.length_visits_le line 442
  25. lemma OAI.ErdosGallai.Batch.VisitChain.edgeSet_eq line 448
  26. theorem OAI.ErdosGallai.Batch.VisitChain.close_cycle line 460
  27. def OAI.ErdosGallai.Batch.CycleVisit.ends line 485
  28. def OAI.ErdosGallai.Batch.CycleVisit.interior line 486
  29. lemma OAI.ErdosGallai.Batch.CycleVisit.separated_of_interiors line 488
  30. theorem OAI.ErdosGallai.Batch.quotient_cycle_inflation line 505
  31. def OAI.ErdosGallai.Batch.VisitChain.of_walk line 523
  32. lemma OAI.ErdosGallai.Batch.VisitChain.of_walk_visits line 531
  33. lemma OAI.ErdosGallai.Batch.VisitChain.of_walk_links line 539
  34. lemma OAI.ErdosGallai.Batch.VisitChain.of_walk_switchEdges line 549
  35. theorem OAI.ErdosGallai.Batch.lift_quotient_cycle line 564
  36. theorem OAI.ErdosGallai.Batch.orient_edge_representatives line 604
  37. def OAI.ErdosGallai.Batch.portFrom line 624
  38. lemma OAI.ErdosGallai.Batch.portFrom_on line 628
  39. theorem OAI.ErdosGallai.Batch.choose_cycle_ports line 636
  40. lemma OAI.ErdosGallai.Batch.last_dart_mem line 669
  41. lemma OAI.ErdosGallai.Batch.cycle_darts_split line 677
  42. theorem OAI.ErdosGallai.Batch.inflate_represented_cycle line 683
  43. theorem OAI.ErdosGallai.Batch.interiors_disjoint_across_routers line 727
  44. def OAI.ErdosGallai.Batch.cyclePortSet line 738
  45. def OAI.ErdosGallai.Batch.visitInterior line 741
  46. theorem OAI.ErdosGallai.Batch.switch_supports_separated line 744
  47. theorem OAI.ErdosGallai.Batch.cyclePortSet_eq_representative_vertices line 770
  48. theorem OAI.ErdosGallai.Batch.complete_batch_cycle line 797