OAI/Combinatorics/MatchingCount/Graphs/Mate.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingFPRAS.Switching.degree_one_card_le_two line 10
  2. theorem OAI.MatchingFPRAS.Switching.degree_one_pair line 34
  3. abbrev OAI.MatchingFPRAS.Switching.Mate line 64
  4. theorem OAI.MatchingFPRAS.Switching.mate_mate line 68
  5. def OAI.MatchingFPRAS.Switching.overlay line 70
  6. theorem OAI.MatchingFPRAS.Switching.overlay_adj line 79
  7. theorem OAI.MatchingFPRAS.Switching.overlay_comm line 82
  8. theorem OAI.MatchingFPRAS.Switching.reachable_mate_left line 86
  9. theorem OAI.MatchingFPRAS.Switching.reachable_mate_right line 92
  10. theorem OAI.MatchingFPRAS.Switching.reachable_mate_left_iff line 97
  11. theorem OAI.MatchingFPRAS.Switching.reachable_mate_right_iff line 105
  12. def OAI.MatchingFPRAS.Switching.switched line 110
  13. theorem OAI.MatchingFPRAS.Switching.switched_apply line 118
  14. theorem OAI.MatchingFPRAS.Switching.overlay_switched line 124
  15. theorem OAI.MatchingFPRAS.Switching.switched_twice line 131
  16. theorem OAI.MatchingFPRAS.Switching.switch_injective line 139
  17. theorem OAI.MatchingFPRAS.Switching.mates_equal_of_adj line 146
  18. theorem OAI.MatchingFPRAS.Switching.mates_equal_of_reachable line 152
  19. theorem OAI.MatchingFPRAS.Switching.mates_ne_of_reachable line 159
  20. theorem OAI.MatchingFPRAS.Switching.overlay_degree_le_two line 163
  21. theorem OAI.MatchingFPRAS.Switching.overlay_degree_one_iff line 177
  22. def OAI.MatchingFPRAS.Switching.restrictMate line 204
  23. theorem OAI.MatchingFPRAS.Switching.restrictMate_apply line 209
  24. theorem OAI.MatchingFPRAS.Switching.overlay_restrict line 213
  25. theorem OAI.MatchingFPRAS.Switching.component_mem_iff line 219
  26. theorem OAI.MatchingFPRAS.Switching.active_component_endpoints line 224
  27. def OAI.MatchingFPRAS.Switching.weight line 270
  28. theorem OAI.MatchingFPRAS.Switching.weight_nonneg line 273
  29. theorem OAI.MatchingFPRAS.Switching.switched_weight line 281
  30. def OAI.MatchingFPRAS.Switching.HasHoles line 291
  31. theorem OAI.MatchingFPRAS.Switching.hasHoles_unique line 293
  32. theorem OAI.MatchingFPRAS.Switching.no_holes_iff line 298
  33. theorem OAI.MatchingFPRAS.Switching.switched_holes_perfect line 301
  34. def OAI.MatchingFPRAS.Switching.matchings line 329
  35. theorem OAI.MatchingFPRAS.Switching.mem_matchings line 332
  36. def OAI.MatchingFPRAS.Switching.partition line 335
  37. theorem OAI.MatchingFPRAS.Switching.partition_nonneg line 338
  38. theorem OAI.MatchingFPRAS.Switching.hole_partition_comparison line 342