OAI/Combinatorics/CycleDecomposition/Decomposition.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ErdosGallai.CycleOrSingleEdge line 13

    Also declared: ComparatorChallenges/CycleDecomposition.lean:15 (same declaration text).

  2. def OAI.ErdosGallai.EdgeDecomposition line 18

    Also declared: ComparatorChallenges/CycleDecomposition.lean:20 (same declaration text).

  3. lemma OAI.ErdosGallai.cycleOrSingleEdge_subset line 27
  4. lemma OAI.ErdosGallai.cycleOrSingleEdge_map line 33
  5. lemma OAI.ErdosGallai.edgeDecomposition_of_indexed line 42
  6. theorem OAI.ErdosGallai.edgeDecomposition_singleEdges line 58
  7. theorem OAI.ErdosGallai.edgeDecomposition_assemble line 69
  8. theorem OAI.ErdosGallai.small_residue line 119
  9. def OAI.ErdosGallai.decompositionCost line 276
  10. lemma OAI.ErdosGallai.decompositionCost_spec line 279
  11. lemma OAI.ErdosGallai.decompositionCost_le line 282
  12. lemma OAI.ErdosGallai.decompositionCost_singleEdges line 285
  13. theorem OAI.ErdosGallai.edgeDecomposition_adjoin line 288
  14. lemma OAI.ErdosGallai.decompositionCost_adjoin line 343
  15. lemma OAI.ErdosGallai.edgeDecomposition_map line 364
  16. lemma OAI.ErdosGallai.decompositionCost_on line 373
  17. lemma OAI.ErdosGallai.edgeDecomposition_on line 389
  18. lemma OAI.ErdosGallai.decompositionCost_adjoin_same line 410
  19. lemma OAI.ErdosGallai.decompositionCost_assemble_same line 428
  20. theorem OAI.ErdosGallai.uniform_piece_cost line 444
  21. theorem OAI.ErdosGallai.uniform_piece_cost_on line 487