OAI/Combinatorics/MatchingCount/Graphs/MatchingMap.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Transport.matching_map_iff line 21
  2. def OAI.MatchingFPRAS.Transport.matchingMap line 46
  3. lemma OAI.MatchingFPRAS.Transport.matchingMap_injective line 49
  4. def OAI.MatchingFPRAS.Transport.edgeExtension line 54
  5. lemma OAI.MatchingFPRAS.Transport.edgeExtension_on line 59
  6. lemma OAI.MatchingFPRAS.Transport.edgeExtension_off line 66
  7. lemma OAI.MatchingFPRAS.Transport.edgeExtension_nonneg line 71
  8. lemma OAI.MatchingFPRAS.Transport.matchingMap_weight line 76
  9. theorem OAI.MatchingFPRAS.Transport.partition_embedding line 84
  10. def OAI.MatchingFPRAS.Enlargement.sourceRealLabel line 130
  11. lemma OAI.MatchingFPRAS.Enlargement.real_edge_not_diag line 135
  12. def OAI.MatchingFPRAS.Enlargement.sourceColoredReal line 143
  13. lemma OAI.MatchingFPRAS.Enlargement.sourceColoredReal_injective line 151
  14. def OAI.MatchingFPRAS.Enlargement.sourceRealEmbedding line 157
  15. def OAI.MatchingFPRAS.Enlargement.sourceRealActivity line 161
  16. def OAI.MatchingFPRAS.Enlargement.sourceRealPortion line 165
  17. lemma OAI.MatchingFPRAS.Enlargement.sourceRealPortion_partition line 168
  18. def OAI.MatchingFPRAS.Enlargement.holeTerminals line 180
  19. def OAI.MatchingFPRAS.Enlargement.holeInternals line 183
  20. lemma OAI.MatchingFPRAS.Enlargement.hole_decomposition line 187
  21. lemma OAI.MatchingFPRAS.Enlargement.survivors_decomposition line 195
  22. lemma OAI.MatchingFPRAS.Enlargement.survivors_empty line 203
  23. lemma OAI.MatchingFPRAS.Enlargement.sourceRealActivity_pos line 209
  24. lemma OAI.MatchingFPRAS.Enlargement.sourceRealPortion_nonneg line 217
  25. lemma OAI.MatchingFPRAS.Enlargement.sourceRealPortion_full line 222
  26. lemma OAI.MatchingFPRAS.Enlargement.sourceRealPortion_full_pos line 229
  27. lemma OAI.MatchingFPRAS.Enlargement.sourceRealPortion_hole_bound line 236
  28. theorem OAI.MatchingFPRAS.Enlargement.source_bag_inflation line 253
  29. def OAI.MatchingFPRAS.Enlargement.bagHeight line 290
  30. lemma OAI.MatchingFPRAS.Enlargement.bagHeight_one line 292
  31. lemma OAI.MatchingFPRAS.Enlargement.bagHeight_pos line 295
  32. lemma OAI.MatchingFPRAS.Enlargement.bagHeight_le line 298
  33. lemma OAI.MatchingFPRAS.Enlargement.bagHeight_adjacent line 304
  34. lemma OAI.MatchingFPRAS.Enlargement.sourceRealActivity_le_strength line 318
  35. lemma OAI.MatchingFPRAS.Enlargement.sourceRealActivity_le_height line 322
  36. lemma OAI.MatchingFPRAS.Enlargement.sourceRealPortion_le_height line 333
  37. def OAI.MatchingFPRAS.Enlargement.sourceBagWeight line 344
  38. lemma OAI.MatchingFPRAS.Enlargement.sourceBagWeight_range line 348
  39. lemma OAI.MatchingFPRAS.Enlargement.sourceBagWeight_global line 360
  40. def OAI.MatchingFPRAS.Enlargement.sourceD line 373
  41. lemma OAI.MatchingFPRAS.Enlargement.sourceD_one line 376
  42. lemma OAI.MatchingFPRAS.Enlargement.sourceD_cast line 384