OAI/Combinatorics/IndependentSets/Fourier/Contexts.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.clauseAnswerEquiv line 10
  2. def OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.clauseAnswerFinEquiv line 16
  3. instance OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.clauseAnswerFintype line 22
  4. instance OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.clauseAnswerInhabited line 25
  5. instance OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.slotFintype line 27
  6. instance OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.slotInhabited line 31
  7. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.card_clauseAnswer line 33
  8. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.card_slot line 37
  9. abbrev OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.I line 39
  10. abbrev OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.J line 40
  11. abbrev OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.ClauseContext line 41
  12. abbrev OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.VariableContext line 42
  13. abbrev OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.SlotContext line 43
  14. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.card_I line 45
  15. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.card_J line 46
  16. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.card_ClauseContext line 47
  17. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.card_VariableContext line 49
  18. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.card_SlotContext line 51
  19. def OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.localConsistent line 54
  20. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.localConsistent_eq_true_iff line 58
  21. def OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.validJ line 65
  22. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.validJ_eq_true_iff line 70
  23. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.validJ_satisfies line 78
  24. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.validJ_consistent line 83
  25. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.validJ_localConsistent line 90
  26. def OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.canonicalSlot line 97
  27. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.canonicalSlot_name line 101
  28. def OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.pi line 113
  29. def OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.sampledVariables line 117
  30. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.sampledVariables_supported line 121
  31. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.sampled_eq_pi line 126
  32. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.sampled_answers_eq_of_visible_eq line 134
  33. def OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.honestJ line 142
  34. def OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.honestI line 146
  35. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.honestJ_valid line 150
  36. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.pi_honest line 162
  37. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.pi_honest_sampled line 170
  38. def OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.baseAccepts line 176
  39. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.baseAccepts_eq_true_iff line 182
  40. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.projection_implies_coordinate_accepts line 190
  41. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.baseAccepts_implies_sampled line 197
  42. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceContexts.projection_implies_sampled_accepts line 207