OAI/Computability/VertexCover/PCP/FiniteGraph.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle line 34
  2. instance OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.instFintypeVertex line 48
  3. instance OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.instFintypeDart line 49
  4. instance OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqVertex line 50
  5. instance OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqDart line 51
  6. instance OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.instNonemptyDart line 52
  7. instance OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.instNonemptyVertex line 54
  8. def OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph line 58
  9. def OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.size line 70
  10. def OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.Satisfiable line 72
  11. def OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.rejectionCount line 74
  12. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.size_positive line 77
  13. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.dartCard_le_size line 80
  14. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_graph line 83
  15. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_size line 87
  16. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_satisfiable line 91
  17. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_rejectionCount line 95
  18. def OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.minimumRejections line 104
  19. def OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.gap line 106
  20. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.exists_minimizer line 108
  21. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.gap_nonnegative line 112
  22. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.gap_le_one line 114
  23. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.gap_eq_zero_iff line 116
  24. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.le_gap_iff line 119
  25. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.inverse_card_le_gap_of_unsatisfiable line 124
  26. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.one_le_dartCard_mul_gap line 128
  27. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.one_le_size_mul_gap line 134
  28. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_minimumRejections line 141
  29. theorem OAI.UniqueGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_gap line 145