OAI/Combinatorics/EuclideanRamsey/NormalCost.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanRamsey.SameOrbit line 32
  2. lemma OAI.EuclideanRamsey.SameOrbit.refl line 33
  3. lemma OAI.EuclideanRamsey.SameOrbit.symm line 34
  4. lemma OAI.EuclideanRamsey.SameOrbit.trans line 37
  5. lemma OAI.EuclideanRamsey.SameOrbit.smul line 42
  6. structure OAI.EuclideanRamsey.NormalCost line 44
  7. lemma OAI.EuclideanRamsey.NormalCost.list_mem line 54
  8. lemma OAI.EuclideanRamsey.NormalCost.list_bound line 56
  9. lemma OAI.EuclideanRamsey.NormalCost.list_bound_const line 65
  10. lemma OAI.EuclideanRamsey.NormalCost.product_difference line 74
  11. lemma OAI.EuclideanRamsey.product_difference_mem line 94
  12. def OAI.EuclideanRamsey.groupList line 108
  13. lemma OAI.EuclideanRamsey.groupList_mem line 110
  14. lemma OAI.EuclideanRamsey.groupList_length line 114
  15. lemma OAI.EuclideanRamsey.groupList_mul_perm line 117
  16. def OAI.EuclideanRamsey.orbitAverage line 126
  17. lemma OAI.EuclideanRamsey.orbitAverage_preserves line 129
  18. lemma OAI.EuclideanRamsey.orbitAverage_derived line 135