OAI/Geometry/CubicTorus/Profiles/CornerGrid155.lean

GitHub source file

114 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.corner_grid_155 line 10
  2. lemma OAI.CubicTorus.corner_grid_156 line 18
  3. lemma OAI.CubicTorus.corner_grid_157 line 26
  4. lemma OAI.CubicTorus.corner_grid_158 line 34
  5. lemma OAI.CubicTorus.corner_grid_159 line 42
  6. lemma OAI.CubicTorus.corner_grid_160 line 50
  7. lemma OAI.CubicTorus.corner_grid_161 line 58
  8. lemma OAI.CubicTorus.corner_grid_162 line 66
  9. lemma OAI.CubicTorus.corner_grid_163 line 74
  10. lemma OAI.CubicTorus.corner_grid_164 line 82
  11. lemma OAI.CubicTorus.corner_grid_165 line 90
  12. lemma OAI.CubicTorus.corner_grid_166 line 98
  13. lemma OAI.CubicTorus.corner_grid_167 line 106
  14. lemma OAI.CubicTorus.corner_grid_168 line 114
  15. lemma OAI.CubicTorus.corner_grid_169 line 122
  16. lemma OAI.CubicTorus.corner_grid_170 line 130
  17. lemma OAI.CubicTorus.corner_grid_171 line 138
  18. lemma OAI.CubicTorus.corner_grid_172 line 146
  19. lemma OAI.CubicTorus.corner_grid_173 line 154
  20. lemma OAI.CubicTorus.corner_grid_174 line 162
  21. lemma OAI.CubicTorus.corner_grid_175 line 170
  22. lemma OAI.CubicTorus.corner_grid_176 line 178
  23. lemma OAI.CubicTorus.corner_grid_177 line 186
  24. lemma OAI.CubicTorus.corner_grid_178 line 194
  25. lemma OAI.CubicTorus.corner_grid_179 line 202
  26. lemma OAI.CubicTorus.corner_grid_180 line 210
  27. lemma OAI.CubicTorus.corner_grid_181 line 218
  28. lemma OAI.CubicTorus.corner_grid_182 line 226
  29. lemma OAI.CubicTorus.corner_grid_183 line 234
  30. lemma OAI.CubicTorus.corner_grid_184 line 242
  31. lemma OAI.CubicTorus.corner_grid_185 line 250
  32. lemma OAI.CubicTorus.corner_grid_186 line 258
  33. lemma OAI.CubicTorus.corner_grid_187 line 266
  34. lemma OAI.CubicTorus.corner_grid_188 line 274
  35. lemma OAI.CubicTorus.corner_grid_189 line 282
  36. lemma OAI.CubicTorus.corner_grid_190 line 290
  37. lemma OAI.CubicTorus.corner_grid_191 line 298
  38. lemma OAI.CubicTorus.corner_grid_192 line 306
  39. lemma OAI.CubicTorus.corner_grid_193 line 314
  40. lemma OAI.CubicTorus.corner_grid_194 line 322
  41. lemma OAI.CubicTorus.corner_grid_195 line 330
  42. lemma OAI.CubicTorus.corner_grid_196 line 338
  43. lemma OAI.CubicTorus.corner_grid_197 line 346
  44. lemma OAI.CubicTorus.corner_grid_198 line 354
  45. lemma OAI.CubicTorus.corner_grid_199 line 362
  46. lemma OAI.CubicTorus.corner_grid_200 line 370
  47. lemma OAI.CubicTorus.corner_grid_201 line 378
  48. lemma OAI.CubicTorus.corner_grid_202 line 386
  49. lemma OAI.CubicTorus.corner_grid_203 line 394
  50. lemma OAI.CubicTorus.corner_grid_204 line 401
  51. lemma OAI.CubicTorus.corner_grid_205 line 408
  52. lemma OAI.CubicTorus.corner_grid_206 line 415
  53. lemma OAI.CubicTorus.corner_grid_207 line 422
  54. lemma OAI.CubicTorus.corner_grid_208 line 430
  55. lemma OAI.CubicTorus.corner_grid_209 line 438
  56. lemma OAI.CubicTorus.corner_grid_210 line 446
  57. lemma OAI.CubicTorus.corner_grid_211 line 454
  58. lemma OAI.CubicTorus.corner_grid_212 line 462
  59. lemma OAI.CubicTorus.corner_grid_213 line 470
  60. lemma OAI.CubicTorus.corner_grid_214 line 478
  61. lemma OAI.CubicTorus.corner_grid_215 line 486
  62. lemma OAI.CubicTorus.corner_grid_216 line 494
  63. lemma OAI.CubicTorus.corner_grid_217 line 502
  64. lemma OAI.CubicTorus.corner_grid_218 line 510
  65. lemma OAI.CubicTorus.corner_grid_219 line 518
  66. lemma OAI.CubicTorus.corner_grid_220 line 526
  67. lemma OAI.CubicTorus.corner_grid_221 line 534
  68. lemma OAI.CubicTorus.corner_grid_222 line 542
  69. lemma OAI.CubicTorus.corner_grid_223 line 550
  70. lemma OAI.CubicTorus.corner_grid_224 line 558
  71. lemma OAI.CubicTorus.corner_grid_225 line 566
  72. lemma OAI.CubicTorus.corner_grid_226 line 574
  73. lemma OAI.CubicTorus.corner_grid_227 line 582
  74. lemma OAI.CubicTorus.corner_grid_228 line 590
  75. lemma OAI.CubicTorus.corner_grid_229 line 598
  76. lemma OAI.CubicTorus.corner_grid_230 line 606
  77. lemma OAI.CubicTorus.corner_grid_231 line 614
  78. lemma OAI.CubicTorus.corner_grid_232 line 622
  79. lemma OAI.CubicTorus.corner_grid_233 line 630
  80. lemma OAI.CubicTorus.corner_grid_234 line 638
  81. lemma OAI.CubicTorus.corner_grid_235 line 644
  82. lemma OAI.CubicTorus.corner_grid_236 line 652
  83. lemma OAI.CubicTorus.corner_grid_237 line 660
  84. lemma OAI.CubicTorus.corner_grid_238 line 668
  85. lemma OAI.CubicTorus.corner_grid_239 line 676
  86. lemma OAI.CubicTorus.corner_grid_240 line 684
  87. lemma OAI.CubicTorus.corner_grid_241 line 692
  88. lemma OAI.CubicTorus.corner_grid_242 line 700
  89. lemma OAI.CubicTorus.corner_grid_243 line 708
  90. lemma OAI.CubicTorus.corner_grid_244 line 714
  91. lemma OAI.CubicTorus.corner_grid_245 line 722
  92. lemma OAI.CubicTorus.corner_grid_246 line 730
  93. lemma OAI.CubicTorus.corner_grid_247 line 738
  94. lemma OAI.CubicTorus.corner_grid_248 line 746
  95. lemma OAI.CubicTorus.corner_grid_249 line 754
  96. lemma OAI.CubicTorus.corner_grid_250 line 762
  97. lemma OAI.CubicTorus.corner_grid_251 line 770
  98. lemma OAI.CubicTorus.corner_grid_252 line 778
  99. lemma OAI.CubicTorus.corner_grid_253 line 786
  100. lemma OAI.CubicTorus.corner_grid_254 line 794
  101. lemma OAI.CubicTorus.corner_grid_255 line 802
  102. lemma OAI.CubicTorus.corner_grid_256 line 810
  103. lemma OAI.CubicTorus.corner_grid_257 line 818
  104. lemma OAI.CubicTorus.corner_grid_258 line 826
  105. lemma OAI.CubicTorus.corner_grid_259 line 834
  106. lemma OAI.CubicTorus.corner_grid_260 line 842
  107. lemma OAI.CubicTorus.corner_grid_261 line 850
  108. lemma OAI.CubicTorus.corner_grid_262 line 856
  109. lemma OAI.CubicTorus.corner_grid_263 line 864
  110. lemma OAI.CubicTorus.corner_grid_264 line 870
  111. lemma OAI.CubicTorus.corner_grid_265 line 878
  112. lemma OAI.CubicTorus.corner_grid_266 line 886
  113. lemma OAI.CubicTorus.corner_grid_267 line 894
  114. lemma OAI.CubicTorus.corner_grid_268 line 902