OAI/Combinatorics/EuclideanRamsey/FiniteEuclidean.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanRamsey.FiniteEuclidean line 28
  2. instance OAI.EuclideanRamsey.FiniteEuclidean.(instance at line 30) line 30
  3. instance OAI.EuclideanRamsey.FiniteEuclidean.(instance at line 31) line 31
  4. def OAI.EuclideanRamsey.FiniteEuclidean.coords line 32
  5. def OAI.EuclideanRamsey.FiniteEuclidean.product line 34
  6. lemma OAI.EuclideanRamsey.FiniteEuclidean.product_eq_sum line 36
  7. instance OAI.EuclideanRamsey.FiniteEuclidean.core line 39
  8. instance OAI.EuclideanRamsey.FiniteEuclidean.(instance at line 66) line 66
  9. instance OAI.EuclideanRamsey.FiniteEuclidean.(instance at line 67) line 67
  10. lemma OAI.EuclideanRamsey.FiniteEuclidean.norm_sq line 68
  11. lemma OAI.EuclideanRamsey.FiniteEuclidean.coords_add line 72
  12. lemma OAI.EuclideanRamsey.FiniteEuclidean.coords_sub line 73
  13. lemma OAI.EuclideanRamsey.FiniteEuclidean.coords_smul line 74
  14. def OAI.EuclideanRamsey.FiniteEuclidean.reindex line 76
  15. def OAI.EuclideanRamsey.FiniteEuclidean.block line 86
  16. def OAI.EuclideanRamsey.FiniteEuclidean.embed line 94
  17. lemma OAI.EuclideanRamsey.FiniteEuclidean.embed_apply line 118
  18. lemma OAI.EuclideanRamsey.FiniteEuclidean.embed_outside line 122
  19. lemma OAI.EuclideanRamsey.FiniteEuclidean.extend_pair line 128
  20. lemma OAI.EuclideanRamsey.FiniteEuclidean.inner_reindex line 143
  21. lemma OAI.EuclideanRamsey.FiniteEuclidean.inner_block_ne line 147
  22. def OAI.EuclideanRamsey.FiniteEuclidean.flatten line 162
  23. lemma OAI.EuclideanRamsey.FiniteEuclidean.norm_sum_blocks line 165
  24. lemma OAI.EuclideanRamsey.FiniteEuclidean.flatten_distance line 177
  25. def OAI.EuclideanRamsey.FiniteEuclidean.unit line 195
  26. lemma OAI.EuclideanRamsey.FiniteEuclidean.norm_unit line 196
  27. lemma OAI.EuclideanRamsey.FiniteEuclidean.inner_unit line 200
  28. lemma OAI.EuclideanRamsey.FiniteEuclidean.common_vertex line 205
  29. lemma OAI.EuclideanRamsey.FiniteEuclidean.unit_distance_constant line 237