OAI/Analysis/Quantum/DimensionTen/BorderRelations.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.Border.C line 10
  2. lemma OAI.DimensionTen.Border.normalize_border line 12
  3. lemma OAI.DimensionTen.Border.E_sum line 20
  4. lemma OAI.DimensionTen.Border.high_shift_0 line 24
  5. lemma OAI.DimensionTen.Border.border_column_0 line 29
  6. lemma OAI.DimensionTen.Border.NB_border_0 line 31
  7. lemma OAI.DimensionTen.Border.high_relation_0 line 34
  8. lemma OAI.DimensionTen.Border.high_shift_1 line 38
  9. lemma OAI.DimensionTen.Border.border_column_1 line 42
  10. lemma OAI.DimensionTen.Border.NB_border_1 line 44
  11. lemma OAI.DimensionTen.Border.high_relation_1 line 47
  12. lemma OAI.DimensionTen.Border.high_shift_2 line 51
  13. lemma OAI.DimensionTen.Border.border_column_2 line 56
  14. lemma OAI.DimensionTen.Border.NB_border_2 line 58
  15. lemma OAI.DimensionTen.Border.high_relation_2 line 61
  16. lemma OAI.DimensionTen.Border.high_shift_3 line 65
  17. lemma OAI.DimensionTen.Border.border_column_3 line 70
  18. lemma OAI.DimensionTen.Border.NB_border_3 line 72
  19. lemma OAI.DimensionTen.Border.high_relation_3 line 75
  20. lemma OAI.DimensionTen.Border.high_shift_4 line 79
  21. lemma OAI.DimensionTen.Border.border_column_4 line 84
  22. lemma OAI.DimensionTen.Border.NB_border_4 line 86
  23. lemma OAI.DimensionTen.Border.high_relation_4 line 89
  24. lemma OAI.DimensionTen.Border.high_shift_5 line 93
  25. lemma OAI.DimensionTen.Border.border_column_5 line 97
  26. lemma OAI.DimensionTen.Border.NB_border_5 line 99
  27. lemma OAI.DimensionTen.Border.high_relation_5 line 102
  28. lemma OAI.DimensionTen.Border.high_shift_6 line 106
  29. lemma OAI.DimensionTen.Border.border_column_6 line 110
  30. lemma OAI.DimensionTen.Border.NB_border_6 line 112
  31. lemma OAI.DimensionTen.Border.high_relation_6 line 115
  32. lemma OAI.DimensionTen.Border.high_shift_7 line 119
  33. lemma OAI.DimensionTen.Border.border_column_7 line 123
  34. lemma OAI.DimensionTen.Border.NB_border_7 line 125
  35. lemma OAI.DimensionTen.Border.high_relation_7 line 128
  36. lemma OAI.DimensionTen.Border.high_shift_8 line 132
  37. lemma OAI.DimensionTen.Border.border_column_8 line 136
  38. lemma OAI.DimensionTen.Border.NB_border_8 line 138
  39. lemma OAI.DimensionTen.Border.high_relation_8 line 141
  40. lemma OAI.DimensionTen.Border.high_shift_9 line 145
  41. lemma OAI.DimensionTen.Border.border_column_9 line 150
  42. lemma OAI.DimensionTen.Border.NB_border_9 line 152
  43. lemma OAI.DimensionTen.Border.high_relation_9 line 155
  44. lemma OAI.DimensionTen.Border.high_shift_10 line 159
  45. lemma OAI.DimensionTen.Border.border_column_10 line 164
  46. lemma OAI.DimensionTen.Border.NB_border_10 line 166
  47. lemma OAI.DimensionTen.Border.high_relation_10 line 169
  48. lemma OAI.DimensionTen.Border.high_shift_11 line 173
  49. lemma OAI.DimensionTen.Border.border_column_11 line 178
  50. lemma OAI.DimensionTen.Border.NB_border_11 line 180
  51. lemma OAI.DimensionTen.Border.high_relation_11 line 183
  52. lemma OAI.DimensionTen.Border.high_shift_12 line 187
  53. lemma OAI.DimensionTen.Border.border_column_12 line 192
  54. lemma OAI.DimensionTen.Border.NB_border_12 line 194
  55. lemma OAI.DimensionTen.Border.high_relation_12 line 197
  56. lemma OAI.DimensionTen.Border.high_shift_13 line 201
  57. lemma OAI.DimensionTen.Border.border_column_13 line 206
  58. lemma OAI.DimensionTen.Border.NB_border_13 line 208
  59. lemma OAI.DimensionTen.Border.high_relation_13 line 211
  60. lemma OAI.DimensionTen.Border.high_shift_14 line 215
  61. lemma OAI.DimensionTen.Border.border_column_14 line 220
  62. lemma OAI.DimensionTen.Border.NB_border_14 line 222
  63. lemma OAI.DimensionTen.Border.high_relation_14 line 225
  64. lemma OAI.DimensionTen.Border.high_relation line 229