OAI/Computability/WeisfeilerLeman/Colors.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLTime.equiv_of_multiset_match line 9
  2. theorem OAI.WLTime.multiset_match_of_equiv line 21
  3. theorem OAI.WLTime.finite_decreasing_choice line 30
  4. theorem OAI.WLTime.tupleColor_eq_of_le line 39
  5. def OAI.WLTime.Stable line 49
  6. theorem OAI.WLTime.equivalent_stable_matching line 52
  7. theorem OAI.WLTime.stable_joint_extension line 64
  8. theorem OAI.WLTime.stable_separate_extension line 80
  9. theorem OAI.WLTime.stable_joint_of_bisimulation line 95
  10. theorem OAI.WLTime.stable_separate_of_bisimulation line 112
  11. def OAI.WLTime.permuteColor line 134
  12. theorem OAI.WLTime.tupleColor_permute line 143
  13. theorem OAI.WLTime.Stable.permute line 169
  14. abbrev OAI.WLTime.Position line 179
  15. def OAI.WLTime.Position.Sub line 181
  16. def OAI.WLTime.Position.PartialIso line 184
  17. structure OAI.WLTime.GameInvariant line 188
  18. def OAI.WLTime.Wins line 195
  19. theorem OAI.WLTime.Wins.forget line 198
  20. theorem OAI.WLTime.Wins.atomic line 203
  21. theorem OAI.WLTime.Wins.extend line 208
  22. def OAI.WLTime.Marks line 215
  23. theorem OAI.WLTime.injective_update_fresh line 218
  24. theorem OAI.WLTime.exists_fresh_slot line 235
  25. theorem OAI.WLTime.atomic_of_wins_marks line 242
  26. theorem OAI.WLTime.joint_color_of_wins line 254
  27. theorem OAI.WLTime.separate_color_of_wins line 286
  28. theorem OAI.WLTime.Position.Sub.refl line 316
  29. theorem OAI.WLTime.Position.Sub.trans line 319
  30. theorem OAI.WLTime.Position.Sub.mark line 328
  31. theorem OAI.WLTime.wins_matching line 335
  32. theorem OAI.WLTime.equivalent_joint_of_wins line 371
  33. theorem OAI.WLTime.equivalent_separate_of_wins line 382
  34. def OAI.WLTime.completePosition line 397
  35. theorem OAI.WLTime.atomic_of_stable line 400
  36. theorem OAI.WLTime.partialIso_of_stable line 408
  37. theorem OAI.WLTime.sub_complete_update line 419
  38. theorem OAI.WLTime.wins_of_stable_separate line 430
  39. theorem OAI.WLTime.separate_stable_iff_wins line 447
  40. theorem OAI.WLTime.wins_of_equivalent_separate line 455
  41. theorem OAI.WLTime.separate_equivalent_iff_wins line 461
  42. theorem OAI.WLTime.factor_injective line 469
  43. theorem OAI.WLTime.projection_factor line 480
  44. def OAI.WLTime.JointFull line 510
  45. theorem OAI.WLTime.update_projection line 513
  46. theorem OAI.WLTime.joint_full_extend line 522
  47. theorem OAI.WLTime.exists_third_slot line 546
  48. theorem OAI.WLTime.partialIso_of_jointFull line 557
  49. theorem OAI.WLTime.wins_of_jointFull line 576
  50. def OAI.WLTime.sparePosition line 593
  51. theorem OAI.WLTime.wins_of_stable_joint line 596
  52. theorem OAI.WLTime.joint_stable_iff_wins line 619
  53. theorem OAI.WLTime.wins_of_equivalent_joint line 629
  54. theorem OAI.WLTime.joint_equivalent_iff_wins line 635
  55. def OAI.WLTime.Graph.degree line 643
  56. theorem OAI.WLTime.Wins.neighborhood_bijection line 646
  57. theorem OAI.WLTime.Wins.degree_eq line 665