OAI/Combinatorics/MatchingCount/Sampling/RelationDestinations.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.relationDestinations line 14
  2. def OAI.MatchingFPRAS.Transport.relationOff line 18
  3. def OAI.MatchingFPRAS.Transport.relationProposal line 22
  4. lemma OAI.MatchingFPRAS.Transport.relationOff_self line 26
  5. lemma OAI.MatchingFPRAS.Transport.relationOff_nonneg line 30
  6. lemma OAI.MatchingFPRAS.Transport.relationOff_sum line 34
  7. lemma OAI.MatchingFPRAS.Transport.relationOff_sum_le_one line 41
  8. lemma OAI.MatchingFPRAS.Transport.relationProposal_nonneg line 49
  9. lemma OAI.MatchingFPRAS.Transport.relationProposal_row line 56
  10. lemma OAI.MatchingFPRAS.Transport.relationProposal_symmetric line 69
  11. def OAI.MatchingFPRAS.Transport.colorProposal line 88
  12. lemma OAI.MatchingFPRAS.Transport.colorProposal_row line 92
  13. lemma OAI.MatchingFPRAS.Transport.colorProposal_symmetric line 96
  14. lemma OAI.MatchingFPRAS.Transport.colorProposal_nonneg line 100
  15. lemma OAI.MatchingFPRAS.Transport.colorProposal_off line 112
  16. theorem OAI.MatchingFPRAS.Transport.colorProposal_dirichlet line 119
  17. lemma OAI.MatchingFPRAS.Transport.TwoEdgeSwitch.symm line 152
  18. lemma OAI.MatchingFPRAS.Transport.TwoEdgeSwitch.normal_form line 162
  19. def OAI.MatchingFPRAS.Transport.edgeEndpoints line 202
  20. lemma OAI.MatchingFPRAS.Transport.edgeEndpoints_spec line 207
  21. def OAI.MatchingFPRAS.Transport.pairRep line 211
  22. lemma OAI.MatchingFPRAS.Transport.pairRep_spec line 217
  23. def OAI.MatchingFPRAS.Transport.withEnds line 223
  24. lemma OAI.MatchingFPRAS.Transport.mem_withEnds line 228
  25. lemma OAI.MatchingFPRAS.Transport.withEnds_card_le line 233
  26. def OAI.MatchingFPRAS.Transport.edgePairOptions line 244
  27. lemma OAI.MatchingFPRAS.Transport.mem_edgePairOptions line 250
  28. lemma OAI.MatchingFPRAS.Transport.edgePairOptions_card_le line 258
  29. def OAI.MatchingFPRAS.Transport.switchOptions line 268
  30. lemma OAI.MatchingFPRAS.Transport.switchOptions_card_le line 279
  31. lemma OAI.MatchingFPRAS.Transport.mem_pairOptions_of_endpoints line 300
  32. lemma OAI.MatchingFPRAS.Transport.inc_eq_ends line 328
  33. lemma OAI.MatchingFPRAS.Transport.switch_mem_options line 332
  34. lemma OAI.MatchingFPRAS.Transport.switchDestinations_card_bound line 365
  35. def OAI.MatchingFPRAS.Transport.switchProposal line 396
  36. lemma OAI.MatchingFPRAS.Transport.switchProposal_row line 400
  37. lemma OAI.MatchingFPRAS.Transport.switchProposal_symmetric line 404
  38. lemma OAI.MatchingFPRAS.Transport.switchProposal_nonneg line 408
  39. lemma OAI.MatchingFPRAS.Transport.switchProposal_off line 421
  40. theorem OAI.MatchingFPRAS.Transport.switchProposal_dirichlet line 427