OAI/Combinatorics/MatchingCount/Graphs/Edge.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingFPRAS.Switching.switched_holes line 11
  2. theorem OAI.MatchingFPRAS.Switching.mixed_hole_partition_comparison line 54
  3. def OAI.MatchingFPRAS.Switching.withEdge line 106
  4. theorem OAI.MatchingFPRAS.Switching.withEdge_apply line 130
  5. theorem OAI.MatchingFPRAS.Switching.withEdge_holes line 136
  6. theorem OAI.MatchingFPRAS.Switching.withEdge_injOn line 150
  7. def OAI.MatchingFPRAS.Switching.edgeActivity line 169
  8. theorem OAI.MatchingFPRAS.Switching.edgeActivity_comm line 172
  9. theorem OAI.MatchingFPRAS.Switching.withEdge_comm line 179
  10. theorem OAI.MatchingFPRAS.Switching.withEdge_weight_of_lt line 192
  11. theorem OAI.MatchingFPRAS.Switching.withEdge_weight line 211
  12. theorem OAI.MatchingFPRAS.Switching.edge_fill_partition line 220
  13. def OAI.MatchingFPRAS.Switching.holeRatio line 243
  14. theorem OAI.MatchingFPRAS.Switching.holeRatio_nonneg line 246
  15. theorem OAI.MatchingFPRAS.Switching.holeRatio_empty line 250
  16. theorem OAI.MatchingFPRAS.Switching.holeRatio_pair_comm line 253
  17. theorem OAI.MatchingFPRAS.Switching.holeRatio_comparison line 257
  18. theorem OAI.MatchingFPRAS.Switching.four_holes line 275
  19. theorem OAI.MatchingFPRAS.Switching.mixed_holeRatio_comparison line 306
  20. theorem OAI.MatchingFPRAS.Switching.edge_fill_holeRatio line 327
  21. def OAI.MatchingFPRAS.Switching.rowMax line 334
  22. theorem OAI.MatchingFPRAS.Switching.holeRatio_le_rowMax line 341
  23. theorem OAI.MatchingFPRAS.Switching.rowMax_attained line 346
  24. theorem OAI.MatchingFPRAS.Switching.two_holes_le_four line 357
  25. theorem OAI.MatchingFPRAS.Switching.four_holes_le_fortyeight line 364
  26. theorem OAI.MatchingFPRAS.Switching.zero_or_two_holes_le_four line 385
  27. theorem OAI.MatchingFPRAS.Switching.small_holes_le_fortyeight line 395
  28. theorem OAI.MatchingFPRAS.Switching.symmDiff_pair_of_mem_mem line 405
  29. theorem OAI.MatchingFPRAS.Switching.symmDiff_pair_of_mem_notMem line 411