OAI/Computability/VertexCover/PCP/PreprocessingCloudIndex.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv line 13
  2. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv_val line 22
  3. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv_symm_apply line 26
  4. def OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts line 30
  5. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.mem_cloudDarts line 33
  6. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_nodup line 37
  7. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_sublist line 41
  8. def OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize line 44
  9. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_le_darts line 46
  10. def OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect line 50
  11. def OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank line 55
  12. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_val line 60
  13. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank_val line 64
  14. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_cloudRank line 68
  15. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank_cloudSelect line 73
  16. def OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudEquiv line 78
  17. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_card_cloud line 85
  18. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_eq_nil_iff line 89
  19. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_zero_iff line 93
  20. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.sum_cloudSize line 97
  21. def OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.oldCloudIndex line 106
  22. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_oldCloudIndex line 109
  23. abbrev OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.PaddedCloud line 113
  24. def OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedOld line 117
  25. def OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedNew line 121
  26. def OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudEquiv line 125
  27. def OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank line 131
  28. def OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect line 135
  29. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_rank line 139
  30. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_select line 144
  31. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old line 149
  32. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new line 154
  33. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old_val line 159
  34. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new_val line 164
  35. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_castAdd line 169
  36. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_natAdd line 181
  37. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingCloudIndex.card_paddedCloud line 187