OAI/Analysis/Quantum/DimensionTen/BorderData.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.Border.H line 9
  2. def OAI.DimensionTen.Border.D line 11
  3. def OAI.DimensionTen.Border.adjH line 13
  4. def OAI.DimensionTen.Border.Cnum line 15
  5. def OAI.DimensionTen.Border.d line 18
  6. def OAI.DimensionTen.Border.detH line 19
  7. def OAI.DimensionTen.Border.B0 line 21
  8. def OAI.DimensionTen.Border.B1 line 24
  9. def OAI.DimensionTen.Border.B2 line 27
  10. def OAI.DimensionTen.Border.B line 30
  11. def OAI.DimensionTen.Border.monExps line 32
  12. def OAI.DimensionTen.Border.mon line 35
  13. def OAI.DimensionTen.Border.low line 38
  14. def OAI.DimensionTen.Border.high line 41
  15. lemma OAI.DimensionTen.Border.commute_01_row0 line 44
  16. lemma OAI.DimensionTen.Border.commute_01_row1 line 45
  17. lemma OAI.DimensionTen.Border.commute_01_row2 line 46
  18. lemma OAI.DimensionTen.Border.commute_01_row3 line 47
  19. lemma OAI.DimensionTen.Border.commute_01_row4 line 48
  20. lemma OAI.DimensionTen.Border.commute_01_row5 line 49
  21. lemma OAI.DimensionTen.Border.commute_01_row6 line 50
  22. lemma OAI.DimensionTen.Border.commute_01_row7 line 51
  23. lemma OAI.DimensionTen.Border.commute_01_row8 line 52
  24. lemma OAI.DimensionTen.Border.commute_01_row9 line 53
  25. lemma OAI.DimensionTen.Border.commute_01_row10 line 54
  26. lemma OAI.DimensionTen.Border.commute_01_row11 line 55
  27. lemma OAI.DimensionTen.Border.commute_01_row12 line 56
  28. lemma OAI.DimensionTen.Border.commute_01_row13 line 57
  29. lemma OAI.DimensionTen.Border.commute_01_row14 line 58
  30. lemma OAI.DimensionTen.Border.commute_01_row15 line 59
  31. lemma OAI.DimensionTen.Border.commute_01_row16 line 60
  32. lemma OAI.DimensionTen.Border.commute_01_row17 line 61
  33. lemma OAI.DimensionTen.Border.commute_01_row18 line 62
  34. lemma OAI.DimensionTen.Border.commute_01_row19 line 63
  35. lemma OAI.DimensionTen.Border.commute_01 line 64
  36. lemma OAI.DimensionTen.Border.commute_02_row0 line 88
  37. lemma OAI.DimensionTen.Border.commute_02_row1 line 89
  38. lemma OAI.DimensionTen.Border.commute_02_row2 line 90
  39. lemma OAI.DimensionTen.Border.commute_02_row3 line 91
  40. lemma OAI.DimensionTen.Border.commute_02_row4 line 92
  41. lemma OAI.DimensionTen.Border.commute_02_row5 line 93
  42. lemma OAI.DimensionTen.Border.commute_02_row6 line 94
  43. lemma OAI.DimensionTen.Border.commute_02_row7 line 95
  44. lemma OAI.DimensionTen.Border.commute_02_row8 line 96
  45. lemma OAI.DimensionTen.Border.commute_02_row9 line 97
  46. lemma OAI.DimensionTen.Border.commute_02_row10 line 98
  47. lemma OAI.DimensionTen.Border.commute_02_row11 line 99
  48. lemma OAI.DimensionTen.Border.commute_02_row12 line 100
  49. lemma OAI.DimensionTen.Border.commute_02_row13 line 101
  50. lemma OAI.DimensionTen.Border.commute_02_row14 line 102
  51. lemma OAI.DimensionTen.Border.commute_02_row15 line 103
  52. lemma OAI.DimensionTen.Border.commute_02_row16 line 104
  53. lemma OAI.DimensionTen.Border.commute_02_row17 line 105
  54. lemma OAI.DimensionTen.Border.commute_02_row18 line 106
  55. lemma OAI.DimensionTen.Border.commute_02_row19 line 107
  56. lemma OAI.DimensionTen.Border.commute_02 line 108
  57. lemma OAI.DimensionTen.Border.commute_12_row0 line 132
  58. lemma OAI.DimensionTen.Border.commute_12_row1 line 133
  59. lemma OAI.DimensionTen.Border.commute_12_row2 line 134
  60. lemma OAI.DimensionTen.Border.commute_12_row3 line 135
  61. lemma OAI.DimensionTen.Border.commute_12_row4 line 136
  62. lemma OAI.DimensionTen.Border.commute_12_row5 line 137
  63. lemma OAI.DimensionTen.Border.commute_12_row6 line 138
  64. lemma OAI.DimensionTen.Border.commute_12_row7 line 139
  65. lemma OAI.DimensionTen.Border.commute_12_row8 line 140
  66. lemma OAI.DimensionTen.Border.commute_12_row9 line 141
  67. lemma OAI.DimensionTen.Border.commute_12_row10 line 142
  68. lemma OAI.DimensionTen.Border.commute_12_row11 line 143
  69. lemma OAI.DimensionTen.Border.commute_12_row12 line 144
  70. lemma OAI.DimensionTen.Border.commute_12_row13 line 145
  71. lemma OAI.DimensionTen.Border.commute_12_row14 line 146
  72. lemma OAI.DimensionTen.Border.commute_12_row15 line 147
  73. lemma OAI.DimensionTen.Border.commute_12_row16 line 148
  74. lemma OAI.DimensionTen.Border.commute_12_row17 line 149
  75. lemma OAI.DimensionTen.Border.commute_12_row18 line 150
  76. lemma OAI.DimensionTen.Border.commute_12_row19 line 151
  77. lemma OAI.DimensionTen.Border.commute_12 line 152
  78. lemma OAI.DimensionTen.Border.inverse_row0 line 176
  79. lemma OAI.DimensionTen.Border.inverse_row1 line 177
  80. lemma OAI.DimensionTen.Border.inverse_row2 line 178
  81. lemma OAI.DimensionTen.Border.inverse_row3 line 179
  82. lemma OAI.DimensionTen.Border.inverse_row4 line 180
  83. lemma OAI.DimensionTen.Border.inverse_row5 line 181
  84. lemma OAI.DimensionTen.Border.inverse_row6 line 182
  85. lemma OAI.DimensionTen.Border.inverse_row7 line 183
  86. lemma OAI.DimensionTen.Border.inverse_row8 line 184
  87. lemma OAI.DimensionTen.Border.inverse_row9 line 185
  88. lemma OAI.DimensionTen.Border.inverse_row10 line 186
  89. lemma OAI.DimensionTen.Border.inverse_row11 line 187
  90. lemma OAI.DimensionTen.Border.inverse_row12 line 188
  91. lemma OAI.DimensionTen.Border.inverse_row13 line 189
  92. lemma OAI.DimensionTen.Border.inverse_row14 line 190
  93. lemma OAI.DimensionTen.Border.inverse line 191
  94. lemma OAI.DimensionTen.Border.relation_row0 line 209
  95. lemma OAI.DimensionTen.Border.relation_row1 line 210
  96. lemma OAI.DimensionTen.Border.relation_row2 line 211
  97. lemma OAI.DimensionTen.Border.relation_row3 line 212
  98. lemma OAI.DimensionTen.Border.relation_row4 line 213
  99. lemma OAI.DimensionTen.Border.relation_row5 line 214
  100. lemma OAI.DimensionTen.Border.relation_row6 line 215
  101. lemma OAI.DimensionTen.Border.relation_row7 line 216
  102. lemma OAI.DimensionTen.Border.relation_row8 line 217
  103. lemma OAI.DimensionTen.Border.relation_row9 line 218
  104. lemma OAI.DimensionTen.Border.relation_row10 line 219
  105. lemma OAI.DimensionTen.Border.relation_row11 line 220
  106. lemma OAI.DimensionTen.Border.relation_row12 line 221
  107. lemma OAI.DimensionTen.Border.relation_row13 line 222
  108. lemma OAI.DimensionTen.Border.relation_row14 line 223
  109. lemma OAI.DimensionTen.Border.relation line 224