OAI/Computability/VertexCover/PCP/VertexPadding.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.VertexPadding.reverseFunction line 15
  2. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.reverseFunction_involutive line 20
  3. def OAI.UniqueGames.Foundations.PCP.VertexPadding.pad line 28
  4. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.pad_tail line 46
  5. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.pad_reverse_inl line 49
  6. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.pad_reverse_inr line 54
  7. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.edgeSatisfied_inl line 58
  8. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.edgeSatisfied_inr line 69
  9. def OAI.UniqueGames.Foundations.PCP.VertexPadding.extendLabeling line 73
  10. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.extendLabeling_inl line 76
  11. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.extendLabeling_inr line 79
  12. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.pad_satisfiable line 82
  13. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.satisfiable_of_pad line 90
  14. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.rejectionCount_eq_sum line 97
  15. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.pad_rejectionCount line 102
  16. def OAI.UniqueGames.Foundations.PCP.VertexPadding.extraVertices line 114
  17. abbrev OAI.UniqueGames.Foundations.PCP.VertexPadding.Vertex line 116
  18. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.card_vertex line 118
  19. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.le_card_vertex line 122
  20. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.card_vertex_le line 126
  21. def OAI.UniqueGames.Foundations.PCP.VertexPadding.familyVertexEquiv line 131
  22. def OAI.UniqueGames.Foundations.PCP.VertexPadding.paddedG line 139
  23. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.paddedG_tail line 142
  24. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.paddedG_rejectionCount line 145
  25. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.rejectionCount_eq line 152
  26. def OAI.UniqueGames.Foundations.PCP.VertexPadding.liftLabel line 159
  27. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.liftLabel_inl line 162
  28. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.liftLabel_inr line 165
  29. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.rejectionCount_liftLabel line 169
  30. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.paddedG_satisfiable line 176
  31. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.card_padded_darts line 180
  32. theorem OAI.UniqueGames.Foundations.PCP.VertexPadding.card_padded_darts_le line 184