OAI/Combinatorics/IndependentSets/Expansion/Finite2.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.sum_card_cloud line 14
  2. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.card_padded_cloud line 18
  3. abbrev OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.dummy line 24
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.card_cloud line 27
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.card_dummy_of_empty line 35
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.card_cloud_of_empty line 39
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.card_cloud_eq_family line 44
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.card_paddedDart_eq_sum line 52
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.card_paddedDart_le line 64
  10. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv line 83
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv_val line 92
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv_symm_apply line 96
  13. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts line 100
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.mem_cloudDarts line 103
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_nodup line 107
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_sublist line 111
  17. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize line 114
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_le_darts line 116
  19. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect line 120
  20. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank line 125
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_val line 130
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank_val line 134
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_cloudRank line 138
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank_cloudSelect line 143
  25. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudEquiv line 148
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_card_cloud line 155
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_eq_nil_iff line 159
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_zero_iff line 163
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.sum_cloudSize line 167
  30. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.oldCloudIndex line 176
  31. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_oldCloudIndex line 179
  32. abbrev OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.PaddedCloud line 183
  33. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedOld line 187
  34. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedNew line 191
  35. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudEquiv line 195
  36. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank line 201
  37. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect line 205
  38. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_rank line 209
  39. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_select line 214
  40. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old line 219
  41. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new line 224
  42. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old_val line 229
  43. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new_val line 234
  44. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_castAdd line 239
  45. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_natAdd line 251
  46. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingCloudIndex.card_paddedCloud line 257