OAI/Combinatorics/MatchingCount/Graphs/Edge2.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.edgeAt line 18
  2. lemma OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.edgeAt_incident line 30
  3. lemma OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.edgeAt_mate line 34
  4. lemma OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.edgeAt_of_incident line 43
  5. def OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.toPM line 49
  6. def OAI.MatchingFPRAS.UnitRefresh.chosenEdge line 60
  7. lemma OAI.MatchingFPRAS.UnitRefresh.chosenEdge_spec line 64
  8. lemma OAI.MatchingFPRAS.UnitRefresh.chosenEdge_unique line 70
  9. def OAI.MatchingFPRAS.UnitRefresh.chosenMate line 75
  10. lemma OAI.MatchingFPRAS.UnitRefresh.chosenMate_pair line 78
  11. lemma OAI.MatchingFPRAS.UnitRefresh.chosenMate_ne line 81
  12. lemma OAI.MatchingFPRAS.UnitRefresh.chosenEdge_chosenMate line 84
  13. lemma OAI.MatchingFPRAS.UnitRefresh.chosenMate_involutive line 90
  14. def OAI.MatchingFPRAS.UnitRefresh.fromPM line 99
  15. lemma OAI.MatchingFPRAS.UnitRefresh.fromPM_edgeAt line 105
  16. lemma OAI.MatchingFPRAS.UnitRefresh.chosenEdge_toPM line 111
  17. def OAI.MatchingFPRAS.UnitRefresh.coloredPMEquiv line 117
  18. theorem OAI.MatchingFPRAS.UnitRefresh.unit_partition_assignments line 145
  19. def OAI.MatchingFPRAS.UnitRefresh.leafBags line 158
  20. def OAI.MatchingFPRAS.UnitRefresh.fiberCount line 163
  21. def OAI.MatchingFPRAS.UnitRefresh.assignmentPartition line 166
  22. def OAI.MatchingFPRAS.UnitRefresh.leafAssignment line 170
  23. def OAI.MatchingFPRAS.UnitRefresh.leafAssignmentEquiv line 179
  24. lemma OAI.MatchingFPRAS.UnitRefresh.fiberCount_sum line 204
  25. lemma OAI.MatchingFPRAS.UnitRefresh.fiberCount_const line 211
  26. lemma OAI.MatchingFPRAS.UnitRefresh.fiberCount_zero line 217
  27. lemma OAI.MatchingFPRAS.UnitRefresh.fiberCount_leaf line 223
  28. lemma OAI.MatchingFPRAS.UnitRefresh.fiberCount_parent line 237
  29. lemma OAI.MatchingFPRAS.UnitRefresh.fiberCount_other line 251
  30. lemma OAI.MatchingFPRAS.UnitRefresh.prod_split_two line 266
  31. lemma OAI.MatchingFPRAS.UnitRefresh.leaf_assignment_weight line 272
  32. lemma OAI.MatchingFPRAS.UnitRefresh.sum_finset_card line 284
  33. def OAI.MatchingFPRAS.UnitRefresh.leafUpdate line 293
  34. theorem OAI.MatchingFPRAS.UnitRefresh.leaf_elimination line 297