OAI/Probability/SwitchChain/ProposalUniqueness.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem315.IsPerfectMatchingOn.mem_iff_exists_adj line 9
  2. theorem OAI.Problem315.IsPerfectMatchingOn.support_unique line 20
  3. theorem OAI.Problem315.SwitchProposal.ext_matchings line 26
  4. theorem OAI.Problem315.removedMatching_adj_iff line 39
  5. theorem OAI.Problem315.addedMatching_adj_iff line 57
  6. theorem OAI.Problem315.proposalResult_injective_on_valid line 73
  7. theorem OAI.Problem315.validSwitch_of_proposalResult_ne line 82
  8. theorem OAI.Problem315.proposalResult_ne_of_validSwitch line 88
  9. theorem OAI.Problem315.validSwitch_iff_proposalResult_ne line 98
  10. theorem OAI.Problem315.proposal_count_eq_one line 102
  11. theorem OAI.Problem315.proposal_count_eq_zero line 125
  12. theorem OAI.Problem315.switchKernel_of_ne line 134