OAI/Combinatorics/CycleDecomposition/ReservoirRemainder.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ErdosGallai.walks_edges_disjoint_of_support line 18
  2. lemma OAI.ErdosGallai.walk_edges_disjoint_spokes_of_outside line 27
  3. lemma OAI.ErdosGallai.walk_edges_disjoint_spokes_of_inside line 40
  4. theorem OAI.ErdosGallai.uniform_reservoir_completion line 53
  5. lemma OAI.ErdosGallai.exists_reservoir_avoided line 117
  6. lemma OAI.ErdosGallai.exists_edge_reservoir_avoided line 139
  7. def OAI.ErdosGallai.reservoirColor line 151
  8. lemma OAI.ErdosGallai.reservoirColor_avoids line 155
  9. def OAI.ErdosGallai.complementaryReservoirGraph line 160
  10. lemma OAI.ErdosGallai.complementaryReservoirGraph_edges line 169
  11. theorem OAI.ErdosGallai.complementary_reservoir_graphs line 178
  12. def OAI.ErdosGallai.reservoirInternal line 209
  13. def OAI.ErdosGallai.reservoirSpokes line 212
  14. lemma OAI.ErdosGallai.mem_reservoirSpokes line 216
  15. lemma OAI.ErdosGallai.reservoirSpokes_card_le line 227
  16. lemma OAI.ErdosGallai.reservoirSpokes_subset line 235
  17. lemma OAI.ErdosGallai.reservoirInternal_spokes_disjoint line 243
  18. theorem OAI.ErdosGallai.reservoir_reservations line 251
  19. lemma OAI.ErdosGallai.complementary_walk_outside line 290
  20. theorem OAI.ErdosGallai.complementary_reservation_ledger line 306
  21. def OAI.ErdosGallai.edgeRestriction line 334
  22. lemma OAI.ErdosGallai.edgeRestriction_le line 339
  23. lemma OAI.ErdosGallai.edgeRestriction_edges line 342
  24. lemma OAI.ErdosGallai.edgeRestriction_edges_of_subset line 347
  25. def OAI.ErdosGallai.completedEdges line 351
  26. def OAI.ErdosGallai.residualInternalGraph line 353
  27. def OAI.ErdosGallai.unusedSpokes line 357
  28. lemma OAI.ErdosGallai.unusedSpokes_card_le line 360
  29. theorem OAI.ErdosGallai.residue_edge_ledger line 367
  30. theorem OAI.ErdosGallai.residue_part_count line 431
  31. lemma OAI.ErdosGallai.induce_edge_image_of_support_subset line 439
  32. theorem OAI.ErdosGallai.residual_induce_exact line 454
  33. lemma OAI.ErdosGallai.walk_edges_internal line 473
  34. lemma OAI.ErdosGallai.completion_edges_subset line 486
  35. lemma OAI.ErdosGallai.completed_subfamilies_disjoint line 508
  36. lemma OAI.ErdosGallai.completed_subfamilies_cover line 526
  37. lemma OAI.ErdosGallai.endpointLoad_family_card line 537
  38. lemma OAI.ErdosGallai.sigma_three_card_le line 549
  39. theorem OAI.ErdosGallai.uniform_three_reservoir_completion line 566
  40. def OAI.ErdosGallai.allReservoirSpokes line 659
  41. lemma OAI.ErdosGallai.coe_allReservoirSpokes line 663
  42. lemma OAI.ErdosGallai.allReservoirSpokes_card_le line 670
  43. theorem OAI.ErdosGallai.three_reservoir_remainder line 680