OAI/Computability/LoopMatching/ExpandBijection.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. def OAI.LoopMatching.SupportedMatching line 11
  2. def OAI.LoopMatching.oldVertex line 15
  3. def OAI.LoopMatching.dummyVertex line 18
  4. lemma OAI.LoopMatching.incident_oldPair line 21
  5. lemma OAI.LoopMatching.oldPair_injective line 29
  6. lemma OAI.LoopMatching.crossPair_injective line 36
  7. lemma OAI.LoopMatching.oldPair_ne_crossPair line 46
  8. lemma OAI.LoopMatching.matching_edge_unique line 54
  9. def OAI.LoopMatching.restrictMatching line 63
  10. lemma OAI.LoopMatching.mem_restrictMatching line 73
  11. lemma OAI.LoopMatching.exists_crossPartner line 78
  12. def OAI.LoopMatching.crossPartner line 97
  13. lemma OAI.LoopMatching.crossPartner_mem line 100
  14. lemma OAI.LoopMatching.crossPartner_eq line 104
  15. lemma OAI.LoopMatching.crossPartner_uncovered line 111
  16. lemma OAI.LoopMatching.crossPartner_injective line 122
  17. lemma OAI.LoopMatching.crossPartner_surjective line 130
  18. def OAI.LoopMatching.dummyEquiv line 170
  19. lemma OAI.LoopMatching.incident_cross_old line 178
  20. lemma OAI.LoopMatching.incident_cross_dummy line 186
  21. lemma OAI.LoopMatching.not_incident_old_dummy line 194
  22. def OAI.LoopMatching.assembledEdges line 204
  23. lemma OAI.LoopMatching.mem_assembledEdges line 209
  24. lemma OAI.LoopMatching.assembledEdges_perfect line 216
  25. def OAI.LoopMatching.assembleMatching line 264
  26. lemma OAI.LoopMatching.restrict_assemble line 272
  27. lemma OAI.LoopMatching.crossPartner_assemble line 288
  28. lemma OAI.LoopMatching.supported_edge_cases line 294
  29. lemma OAI.LoopMatching.assemble_restrict line 315
  30. instance OAI.LoopMatching.supportedMatchingFintype line 329
  31. def OAI.LoopMatching.assembleMatchingEquiv line 334
  32. def OAI.LoopMatching.supportedMatchingEquiv line 352
  33. lemma OAI.LoopMatching.supportedMatchingEquiv_fst line 356
  34. def OAI.LoopMatching.supportedEdgeEquiv line 363
  35. lemma OAI.LoopMatching.supported_matching_weight line 386
  36. lemma OAI.LoopMatching.unsupported_matching_weight_zero line 414