OAI/Computability/LoopMatching/LiteralChoices.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. def OAI.LoopMatching.OrdinaryChoices line 12
  2. def OAI.LoopMatching.LoopChoices line 15
  3. def OAI.LoopMatching.MatchingChoices line 18
  4. def OAI.LoopMatching.Choices line 21
  5. instance OAI.LoopMatching.ordinaryChoicesFintype line 24
  6. instance OAI.LoopMatching.loopChoicesFintype line 30
  7. instance OAI.LoopMatching.matchingChoicesFintype line 36
  8. instance OAI.LoopMatching.choicesFintype line 41
  9. theorem OAI.LoopMatching.card_ordinaryChoices line 45
  10. theorem OAI.LoopMatching.card_loopChoices line 52
  11. theorem OAI.LoopMatching.card_matchingChoices line 59
  12. theorem OAI.LoopMatching.count_eq_card_choices line 65