OAI/Combinatorics/MatchingCount/Graphs/EdgeLow.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.edgeLow line 19
  2. def OAI.MatchingFPRAS.Transport.edgeHigh line 21
  3. lemma OAI.MatchingFPRAS.Transport.edgeLow_mk line 24
  4. lemma OAI.MatchingFPRAS.Transport.edgeHigh_mk line 27
  5. lemma OAI.MatchingFPRAS.Transport.edgeLow_mem line 30
  6. lemma OAI.MatchingFPRAS.Transport.edgeHigh_mem line 35
  7. lemma OAI.MatchingFPRAS.Transport.edge_low_high line 40
  8. lemma OAI.MatchingFPRAS.Transport.edgeLow_lt_high line 45
  9. lemma OAI.MatchingFPRAS.Transport.edgeLow_ne_high line 54
  10. def OAI.MatchingFPRAS.Transport.pickedEdge line 57
  11. lemma OAI.MatchingFPRAS.Transport.pickedEdge_spec line 61
  12. lemma OAI.MatchingFPRAS.Transport.pickedEdge_unique line 66
  13. def OAI.MatchingFPRAS.Transport.partialMateFun line 70
  14. lemma OAI.MatchingFPRAS.Transport.partialMateFun_out line 73
  15. lemma OAI.MatchingFPRAS.Transport.partialMateFun_ne line 77
  16. lemma OAI.MatchingFPRAS.Transport.partialMateFun_pair line 81
  17. lemma OAI.MatchingFPRAS.Transport.partialMateFun_incident line 86
  18. lemma OAI.MatchingFPRAS.Transport.partialMateFun_covered line 91
  19. lemma OAI.MatchingFPRAS.Transport.partialMateFun_involutive line 99
  20. def OAI.MatchingFPRAS.Transport.partialMate line 111
  21. lemma OAI.MatchingFPRAS.Transport.partialMate_holes line 113
  22. lemma OAI.MatchingFPRAS.Transport.partialMate_low line 121
  23. lemma OAI.MatchingFPRAS.Transport.partial_low_mem line 126
  24. lemma OAI.MatchingFPRAS.Transport.partial_low_injective line 133
  25. lemma OAI.MatchingFPRAS.Transport.partial_low_surjective line 138
  26. lemma OAI.MatchingFPRAS.Transport.partial_card line 150
  27. lemma OAI.MatchingFPRAS.Transport.partial_even line 159
  28. lemma OAI.MatchingFPRAS.Transport.partial_weight line 163
  29. theorem OAI.MatchingFPRAS.Transport.partial_height_le_capacity line 175
  30. def OAI.MatchingFPRAS.Transport.bagEdgeSigmaEquiv line 198
  31. lemma OAI.MatchingFPRAS.Transport.bag_color_card_le_two line 205
  32. theorem OAI.MatchingFPRAS.Transport.bagEdge_card_le_square line 217
  33. def OAI.MatchingFPRAS.Transport.inflationScale line 242
  34. theorem OAI.MatchingFPRAS.Transport.bag_inflation_of_hole_estimate line 244
  35. lemma OAI.MatchingFPRAS.RealGeometry.edge_incident_internal line 310
  36. lemma OAI.MatchingFPRAS.RealGeometry.edge_incident_terminal line 324
  37. def OAI.MatchingFPRAS.RealGeometry.selectedSet line 331
  38. lemma OAI.MatchingFPRAS.RealGeometry.mem_selectedSet line 336
  39. def OAI.MatchingFPRAS.RealGeometry.survivors line 340
  40. lemma OAI.MatchingFPRAS.RealGeometry.mem_survivors_terminal line 347
  41. lemma OAI.MatchingFPRAS.RealGeometry.mem_survivors_internal line 351
  42. lemma OAI.MatchingFPRAS.RealGeometry.internal_unique_iff line 355
  43. lemma OAI.MatchingFPRAS.RealGeometry.terminal_selected_iff line 378
  44. lemma OAI.MatchingFPRAS.RealGeometry.terminal_unique_iff line 392
  45. theorem OAI.MatchingFPRAS.RealGeometry.family_iff_matching line 422
  46. def OAI.MatchingFPRAS.RealGeometry.selectionEquiv line 481
  47. def OAI.MatchingFPRAS.RealGeometry.realMatchingEquiv line 491
  48. lemma OAI.MatchingFPRAS.RealGeometry.selectedSet_weight line 497
  49. theorem OAI.MatchingFPRAS.RealGeometry.realMatching_partition line 503