OAI/Combinatorics/IndependentSets/PCP/VertexPadding.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.reverseFunction line 12
  2. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.reverseFunction_involutive line 17
  3. def OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.pad line 25
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.pad_tail line 43
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.pad_reverse_inl line 46
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.pad_reverse_inr line 51
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.edgeSatisfied_inl line 55
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.edgeSatisfied_inr line 66
  9. def OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.extendLabeling line 70
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.extendLabeling_inl line 73
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.extendLabeling_inr line 76
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.pad_satisfiable line 79
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.satisfiable_of_pad line 87
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.rejectionCount_eq_sum line 94
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.pad_rejectionCount line 99
  16. def OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.extraVertices line 111
  17. abbrev OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.Vertex line 113
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.card_vertex line 115
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.le_card_vertex line 119
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.card_vertex_le line 123
  21. def OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.familyVertexEquiv line 128
  22. def OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.paddedG line 136
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.paddedG_tail line 139
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.paddedG_rejectionCount line 142
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.rejectionCount_eq line 149
  26. def OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.liftLabel line 156
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.liftLabel_inl line 159
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.liftLabel_inr line 162
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.rejectionCount_liftLabel line 166
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.paddedG_satisfiable line 173
  31. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.card_padded_darts line 177
  32. theorem OAI.IndependentSetsGames.Foundations.PCP.VertexPadding.card_padded_darts_le line 181