OAI/Combinatorics/VariableWL/GeneralReduction.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Blocks.completeList line 12
  2. theorem OAI.VariableWL.Blocks.completeList_mem line 18
  3. def OAI.VariableWL.Blocks.GlobalPool line 24
  4. theorem OAI.VariableWL.Blocks.globalPool_nonempty line 28
  5. theorem OAI.VariableWL.Blocks.globalPool_down line 36
  6. theorem OAI.VariableWL.Blocks.globalPool_extend line 44
  7. def OAI.VariableWL.General.numberedTranslation line 66
  8. def OAI.VariableWL.General.numberedPart line 70
  9. theorem OAI.VariableWL.General.numberedTranslation_local line 73
  10. theorem OAI.VariableWL.General.winning_of_witness line 87
  11. theorem OAI.VariableWL.General.base_card_equal line 120
  12. theorem OAI.VariableWL.General.base_neighbors_lt line 127
  13. theorem OAI.VariableWL.General.base_degree_quotient line 132
  14. theorem OAI.VariableWL.General.base_degree_gt_one line 144
  15. def OAI.VariableWL.General.numberedIso line 156
  16. theorem OAI.VariableWL.General.recognized_base line 166
  17. def OAI.VariableWL.General.zeroQuery line 198
  18. def OAI.VariableWL.General.valuationQuery line 201
  19. theorem OAI.VariableWL.General.zeroQuery_injective line 205
  20. theorem OAI.VariableWL.General.zeroQuery_recognized line 210
  21. theorem OAI.VariableWL.General.zeroQuery_agree line 217
  22. def OAI.VariableWL.Game.Ring line 252
  23. theorem OAI.VariableWL.Game.ring_nonempty line 265
  24. theorem OAI.VariableWL.Game.Ring.compatible line 277
  25. theorem OAI.VariableWL.Game.Ring.replace line 284
  26. theorem OAI.VariableWL.Game.Ring.replace_all line 312
  27. theorem OAI.VariableWL.Game.sigma_eq_cast line 344
  28. def OAI.VariableWL.Game.decodeSigma line 349
  29. def OAI.VariableWL.Game.RingLists line 351
  30. theorem OAI.VariableWL.Game.ringLists_nonempty line 364
  31. theorem OAI.VariableWL.Game.ringLists_compatible line 371
  32. theorem OAI.VariableWL.Game.ringLists_transfer line 380