OAI/Combinatorics/CycleDecomposition/ExpansionBoxes.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ErdosGallai.Scale.avoidGraph line 16
  2. lemma OAI.ErdosGallai.Scale.chain_reachable line 21
  3. theorem OAI.ErdosGallai.Scale.connector_exists line 35
  4. lemma OAI.ErdosGallai.Scale.avoid_support line 103
  5. theorem OAI.ErdosGallai.Scale.shortest_set_connector line 114
  6. lemma OAI.ErdosGallai.Scale.path_cons_append line 148
  7. theorem OAI.ErdosGallai.Scale.cycle_across_middle line 160
  8. theorem OAI.ErdosGallai.Scale.long_cycle_of_vertex_expansion line 226
  9. def OAI.ErdosGallai.Scale.SupportedOn line 337
  10. structure OAI.ErdosGallai.Scale.AssignedPiece line 340
  11. def OAI.ErdosGallai.Scale.restrictGraph line 345
  12. def OAI.ErdosGallai.Scale.crossingGraph line 350
  13. def OAI.ErdosGallai.Scale.edgeOccurrences line 356
  14. def OAI.ErdosGallai.Scale.GraphPartition line 360
  15. def OAI.ErdosGallai.Scale.edgeCount line 363
  16. def OAI.ErdosGallai.Scale.cutCount line 367
  17. def OAI.ErdosGallai.Scale.CutExpansionOn line 371
  18. lemma OAI.ErdosGallai.Scale.edgeOccurrences_nil line 374
  19. lemma OAI.ErdosGallai.Scale.edgeOccurrences_cons line 377
  20. lemma OAI.ErdosGallai.Scale.edgeOccurrences_append line 381
  21. lemma OAI.ErdosGallai.Scale.restrictGraph_le line 386
  22. lemma OAI.ErdosGallai.Scale.restrictGraph_supported line 388
  23. lemma OAI.ErdosGallai.Scale.partition_member_le line 391
  24. lemma OAI.ErdosGallai.Scale.edgeCount_bot line 402
  25. def OAI.ErdosGallai.Scale.splitPotential line 411
  26. lemma OAI.ErdosGallai.Scale.logb_four_thirds line 414
  27. lemma OAI.ErdosGallai.Scale.splitPotential_bounds line 422
  28. lemma OAI.ErdosGallai.Scale.splitPotential_monotone line 441
  29. lemma OAI.ErdosGallai.Scale.split_potential_decrement line 452
  30. lemma OAI.ErdosGallai.Scale.split_potential_subadditive line 482
  31. def OAI.ErdosGallai.Scale.externalOn line 503
  32. lemma OAI.ErdosGallai.Scale.externalOn_subset line 506
  33. lemma OAI.ErdosGallai.Scale.externalOn_disjoint line 512
  34. lemma OAI.ErdosGallai.Scale.overlap_child_supported line 518
  35. lemma OAI.ErdosGallai.Scale.overlap_child_sizes line 533
  36. lemma OAI.ErdosGallai.Scale.partition_split_append line 574
  37. theorem OAI.ErdosGallai.Scale.box_recursion line 584