OAI/Combinatorics/IndependentSets/PCP/InitialGraph.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.Label line 11
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.Vertex line 12
  3. abbrev OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.Dart line 13
  4. instance OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.slotFintype line 15
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.card_slot line 19
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.card_label line 20
  7. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.variableVertex line 23
  8. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.clauseVertex line 24
  9. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.dummyVertex line 25
  10. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.dummyDart line 26
  11. instance OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.vertexNonempty line 28
  12. instance OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.dartNonempty line 29
  13. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.reverse line 31
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.reverse_involutive line 35
  15. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.reverseEquiv line 41
  16. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.tail line 47
  17. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.toClauseAnswer line 52
  18. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.fromClauseAnswer line 53
  19. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.variableLabel line 54
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.to_fromClauseAnswer line 56
  21. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.variableValid line 60
  22. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.incidenceAccept line 63
  23. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.predicate line 69
  24. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.raw line 74
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.raw_forward line 85
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.incidenceAccept_true line 90
  27. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.honestLabeling line 97
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.incidence_honest line 102
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.raw_completeness line 110
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.clauseAnswer_eq_of_slots line 119
  31. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.raw_reflects line 128
  32. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.raw_satisfiable_iff line 147
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.card_vertex line 150
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.card_dart line 154
  35. abbrev OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.CompactVertex line 159
  36. abbrev OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.CompactDart line 160
  37. def OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.build line 162
  38. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.build_satisfiable_iff line 165
  39. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.build_vertex_bound line 169
  40. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.build_dart_count line 175
  41. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.build_initial_gap line 179
  42. theorem OAI.IndependentSetsGames.Foundations.PCP.InitialGraph.build_inverse_size_gap line 185