OAI/Combinatorics/VariableWL/Refinement.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.map_univ_comp_equiv line 9
  2. def OAI.VariableWL.tupleEquiv line 15
  3. theorem OAI.VariableWL.color_iso line 22
  4. theorem OAI.VariableWL.histogram_iso line 43
  5. theorem OAI.VariableWL.equivalent_of_iso line 51
  6. theorem OAI.VariableWL.histogram_card line 54
  7. theorem OAI.VariableWL.equivalent_order line 58
  8. theorem OAI.VariableWL.color_zero_eq_iff line 64
  9. theorem OAI.VariableWL.exists_color_match line 85
  10. theorem OAI.VariableWL.iso_of_equivalent_large line 94
  11. theorem OAI.VariableWL.equivalent_large_iff_iso line 124
  12. def OAI.VariableWL.defaultColor line 136
  13. instance OAI.VariableWL.colorInhabited line 140
  14. abbrev OAI.VariableWL.TaggedTuple line 142
  15. def OAI.VariableWL.tagColor line 144
  16. def OAI.VariableWL.liftColor line 147
  17. theorem OAI.VariableWL.color_factor_succ line 150
  18. theorem OAI.VariableWL.tagColor_factor_succ line 163
  19. theorem OAI.VariableWL.tagColor_eq_previous line 170
  20. def OAI.VariableWL.StableAt line 176
  21. def OAI.VariableWL.samePairs line 179
  22. theorem OAI.VariableWL.samePairs_next_subset line 184
  23. theorem OAI.VariableWL.exists_nat_plateau line 191
  24. theorem OAI.VariableWL.exists_stable_round line 209
  25. theorem OAI.VariableWL.stable_later_factor line 230
  26. theorem OAI.VariableWL.histogram_fst line 248
  27. theorem OAI.VariableWL.histogram_eq_previous line 252
  28. theorem OAI.VariableWL.histogram_eq_of_le line 257
  29. theorem OAI.VariableWL.histogram_eq_later line 266
  30. theorem OAI.VariableWL.equivalent_iff_bounded_round line 282
  31. theorem OAI.VariableWL.exists_equiv_of_map_univ_eq line 301
  32. def OAI.VariableWL.permColor line 313
  33. theorem OAI.VariableWL.color_reindex line 319
  34. def OAI.VariableWL.StableEq line 337
  35. theorem OAI.VariableWL.StableEq.reindex line 340
  36. theorem OAI.VariableWL.color_eq_previous line 345
  37. theorem OAI.VariableWL.color_eq_of_le line 349
  38. theorem OAI.VariableWL.stableEq_of_color_eq line 359
  39. theorem OAI.VariableWL.StableEq.exists_bijection line 369
  40. abbrev OAI.VariableWL.Game.Position line 387
  41. def OAI.VariableWL.Game.PartialIso line 389
  42. def OAI.VariableWL.Game.Subposition line 393
  43. def OAI.VariableWL.Game.WinningFamily line 396
  44. def OAI.VariableWL.Game.Winning line 402
  45. theorem OAI.VariableWL.Game.Winning.partialIso line 405
  46. theorem OAI.VariableWL.Game.Winning.discard line 410
  47. theorem OAI.VariableWL.Game.Winning.move line 415
  48. theorem OAI.VariableWL.Game.clear_subposition line 423
  49. def OAI.VariableWL.Game.Realizes line 430
  50. theorem OAI.VariableWL.Game.exists_fresh line 434
  51. theorem OAI.VariableWL.Game.update_injective_of_fresh line 441
  52. theorem OAI.VariableWL.Game.Winning.color_eq line 456
  53. theorem OAI.VariableWL.Game.Subposition.refl line 490
  54. theorem OAI.VariableWL.Game.Subposition.trans line 493
  55. theorem OAI.VariableWL.Game.place_extends line 497
  56. def OAI.VariableWL.Game.triangularEquiv line 505
  57. theorem OAI.VariableWL.Game.Winning.fill line 512
  58. theorem OAI.VariableWL.Game.equivalent_of_winning line 549
  59. theorem OAI.VariableWL.Game.reindex_embeddings line 565
  60. def OAI.VariableWL.Game.FullStable line 578
  61. theorem OAI.VariableWL.Game.fullStable_update line 582
  62. theorem OAI.VariableWL.Game.FullStable.atomic line 627
  63. def OAI.VariableWL.Game.Fits line 644
  64. def OAI.VariableWL.Game.GhostFamily line 648
  65. theorem OAI.VariableWL.Game.ghostFamily_winning line 651
  66. theorem OAI.VariableWL.Game.exists_fullStable line 676
  67. theorem OAI.VariableWL.Game.winning_of_equivalent line 696
  68. theorem OAI.VariableWL.Game.equivalent_iff_winning line 704
  69. inductive OAI.VariableWL.Game.Action line 713
  70. def OAI.VariableWL.Game.historyPosition line 717
  71. abbrev OAI.VariableWL.Game.Strategy line 722
  72. inductive OAI.VariableWL.Game.Reached line 725
  73. def OAI.VariableWL.Game.StrategyWins line 733
  74. theorem OAI.VariableWL.Game.winning_of_strategy line 737
  75. def OAI.VariableWL.Game.invariantStrategy line 750
  76. theorem OAI.VariableWL.Game.invariantStrategy_reached line 755
  77. theorem OAI.VariableWL.Game.strategy_of_winning line 771
  78. theorem OAI.VariableWL.Game.empty_winning_iff_strategy line 784
  79. theorem OAI.VariableWL.Game.wl_iff_announced_strategy line 789