OAI/Geometry/CubicTorus/Profiles/CornerGrid381.lean

GitHub source file

143 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.corner_grid_381 line 10
  2. lemma OAI.CubicTorus.corner_grid_382 line 18
  3. lemma OAI.CubicTorus.corner_grid_383 line 26
  4. lemma OAI.CubicTorus.corner_grid_384 line 34
  5. lemma OAI.CubicTorus.corner_grid_385 line 42
  6. lemma OAI.CubicTorus.corner_grid_386 line 50
  7. lemma OAI.CubicTorus.corner_grid_387 line 58
  8. lemma OAI.CubicTorus.corner_grid_388 line 66
  9. lemma OAI.CubicTorus.corner_grid_389 line 74
  10. lemma OAI.CubicTorus.corner_grid_390 line 82
  11. lemma OAI.CubicTorus.corner_grid_391 line 90
  12. lemma OAI.CubicTorus.corner_grid_392 line 98
  13. lemma OAI.CubicTorus.corner_grid_393 line 106
  14. lemma OAI.CubicTorus.corner_grid_394 line 114
  15. lemma OAI.CubicTorus.corner_grid_395 line 122
  16. lemma OAI.CubicTorus.corner_grid_396 line 130
  17. lemma OAI.CubicTorus.corner_grid_397 line 138
  18. lemma OAI.CubicTorus.corner_grid_398 line 146
  19. lemma OAI.CubicTorus.corner_grid_399 line 154
  20. lemma OAI.CubicTorus.corner_grid_400 line 162
  21. lemma OAI.CubicTorus.corner_grid_401 line 170
  22. lemma OAI.CubicTorus.corner_grid_402 line 178
  23. lemma OAI.CubicTorus.corner_grid_403 line 186
  24. lemma OAI.CubicTorus.corner_grid_404 line 194
  25. lemma OAI.CubicTorus.corner_grid_405 line 202
  26. lemma OAI.CubicTorus.corner_grid_406 line 210
  27. lemma OAI.CubicTorus.corner_grid_407 line 218
  28. lemma OAI.CubicTorus.corner_grid_408 line 226
  29. lemma OAI.CubicTorus.corner_grid_409 line 234
  30. lemma OAI.CubicTorus.corner_grid_410 line 242
  31. lemma OAI.CubicTorus.corner_grid_411 line 250
  32. lemma OAI.CubicTorus.corner_grid_412 line 258
  33. lemma OAI.CubicTorus.corner_grid_413 line 266
  34. lemma OAI.CubicTorus.corner_grid_414 line 274
  35. lemma OAI.CubicTorus.corner_grid_415 line 282
  36. lemma OAI.CubicTorus.corner_grid_416 line 290
  37. lemma OAI.CubicTorus.corner_grid_417 line 298
  38. lemma OAI.CubicTorus.corner_grid_418 line 306
  39. lemma OAI.CubicTorus.corner_grid_419 line 314
  40. lemma OAI.CubicTorus.corner_grid_420 line 322
  41. lemma OAI.CubicTorus.corner_grid_421 line 330
  42. lemma OAI.CubicTorus.corner_grid_422 line 338
  43. lemma OAI.CubicTorus.corner_grid_423 line 346
  44. lemma OAI.CubicTorus.corner_grid_424 line 354
  45. lemma OAI.CubicTorus.corner_grid_425 line 362
  46. lemma OAI.CubicTorus.corner_grid_426 line 370
  47. lemma OAI.CubicTorus.corner_grid_427 line 378
  48. lemma OAI.CubicTorus.corner_grid_428 line 386
  49. lemma OAI.CubicTorus.corner_grid_429 line 394
  50. lemma OAI.CubicTorus.corner_grid_430 line 402
  51. lemma OAI.CubicTorus.corner_grid_431 line 410
  52. lemma OAI.CubicTorus.corner_grid_432 line 418
  53. lemma OAI.CubicTorus.corner_grid_433 line 426
  54. lemma OAI.CubicTorus.corner_grid_434 line 434
  55. lemma OAI.CubicTorus.corner_grid_435 line 442
  56. lemma OAI.CubicTorus.corner_grid_436 line 450
  57. lemma OAI.CubicTorus.corner_grid_437 line 458
  58. lemma OAI.CubicTorus.corner_grid_438 line 466
  59. lemma OAI.CubicTorus.corner_grid_439 line 474
  60. lemma OAI.CubicTorus.corner_grid_440 line 482
  61. lemma OAI.CubicTorus.corner_grid_441 line 490
  62. lemma OAI.CubicTorus.corner_grid_442 line 498
  63. lemma OAI.CubicTorus.corner_grid_443 line 506
  64. lemma OAI.CubicTorus.corner_grid_444 line 514
  65. lemma OAI.CubicTorus.corner_grid_445 line 522
  66. lemma OAI.CubicTorus.corner_grid_446 line 530
  67. lemma OAI.CubicTorus.corner_grid_447 line 538
  68. lemma OAI.CubicTorus.corner_grid_448 line 546
  69. lemma OAI.CubicTorus.corner_grid_449 line 554
  70. lemma OAI.CubicTorus.corner_grid_450 line 562
  71. lemma OAI.CubicTorus.corner_grid_451 line 570
  72. lemma OAI.CubicTorus.corner_grid_452 line 578
  73. lemma OAI.CubicTorus.corner_grid_453 line 586
  74. lemma OAI.CubicTorus.corner_grid_454 line 594
  75. lemma OAI.CubicTorus.corner_grid_455 line 602
  76. lemma OAI.CubicTorus.corner_grid_456 line 610
  77. lemma OAI.CubicTorus.corner_grid_457 line 618
  78. lemma OAI.CubicTorus.corner_grid_458 line 626
  79. lemma OAI.CubicTorus.corner_grid_459 line 634
  80. lemma OAI.CubicTorus.corner_grid_460 line 642
  81. lemma OAI.CubicTorus.corner_grid_461 line 650
  82. lemma OAI.CubicTorus.corner_grid_462 line 658
  83. lemma OAI.CubicTorus.corner_grid_463 line 666
  84. lemma OAI.CubicTorus.corner_grid_464 line 674
  85. lemma OAI.CubicTorus.corner_grid_465 line 682
  86. lemma OAI.CubicTorus.corner_grid_466 line 690
  87. lemma OAI.CubicTorus.corner_grid_467 line 698
  88. lemma OAI.CubicTorus.corner_grid_468 line 706
  89. lemma OAI.CubicTorus.corner_grid_469 line 714
  90. lemma OAI.CubicTorus.corner_grid_470 line 722
  91. lemma OAI.CubicTorus.corner_grid_471 line 730
  92. lemma OAI.CubicTorus.corner_grid_472 line 738
  93. lemma OAI.CubicTorus.corner_grid_473 line 746
  94. lemma OAI.CubicTorus.corner_grid_474 line 754
  95. lemma OAI.CubicTorus.corner_grid_475 line 762
  96. lemma OAI.CubicTorus.corner_grid_476 line 770
  97. lemma OAI.CubicTorus.corner_grid_477 line 778
  98. lemma OAI.CubicTorus.corner_grid_478 line 786
  99. lemma OAI.CubicTorus.corner_grid_479 line 794
  100. lemma OAI.CubicTorus.corner_grid_480 line 802
  101. lemma OAI.CubicTorus.corner_grid_481 line 810
  102. lemma OAI.CubicTorus.corner_grid_482 line 818
  103. lemma OAI.CubicTorus.corner_grid_483 line 826
  104. lemma OAI.CubicTorus.corner_grid_484 line 834
  105. lemma OAI.CubicTorus.corner_grid_485 line 842
  106. lemma OAI.CubicTorus.corner_grid_486 line 850
  107. lemma OAI.CubicTorus.corner_grid_487 line 858
  108. lemma OAI.CubicTorus.corner_grid_488 line 864
  109. lemma OAI.CubicTorus.corner_grid_489 line 872
  110. lemma OAI.CubicTorus.corner_grid_490 line 880
  111. lemma OAI.CubicTorus.corner_grid_491 line 888
  112. lemma OAI.CubicTorus.corner_grid_492 line 896
  113. lemma OAI.CubicTorus.corner_grid_493 line 904
  114. lemma OAI.CubicTorus.corner_grid_494 line 912
  115. lemma OAI.CubicTorus.corner_grid_495 line 920
  116. lemma OAI.CubicTorus.corner_grid_496 line 928
  117. lemma OAI.CubicTorus.corner_grid_497 line 936
  118. lemma OAI.CubicTorus.corner_grid_498 line 944
  119. lemma OAI.CubicTorus.corner_grid_499 line 950
  120. lemma OAI.CubicTorus.corner_grid_500 line 958
  121. lemma OAI.CubicTorus.corner_grid_501 line 966
  122. lemma OAI.CubicTorus.corner_grid_502 line 972
  123. lemma OAI.CubicTorus.corner_grid_503 line 980
  124. lemma OAI.CubicTorus.corner_grid_504 line 986
  125. lemma OAI.CubicTorus.corner_grid_505 line 994
  126. lemma OAI.CubicTorus.corner_grid_506 line 1002
  127. lemma OAI.CubicTorus.corner_grid_507 line 1010
  128. lemma OAI.CubicTorus.corner_grid_508 line 1018
  129. lemma OAI.CubicTorus.corner_grid_509 line 1026
  130. lemma OAI.CubicTorus.corner_grid_510 line 1034
  131. lemma OAI.CubicTorus.corner_grid_511 line 1040
  132. lemma OAI.CubicTorus.corner_grid_512 line 1048
  133. lemma OAI.CubicTorus.corner_grid_513 line 1056
  134. lemma OAI.CubicTorus.corner_grid_514 line 1062
  135. lemma OAI.CubicTorus.corner_grid_515 line 1070
  136. lemma OAI.CubicTorus.corner_grid_516 line 1076
  137. lemma OAI.CubicTorus.corner_grid_517 line 1084
  138. lemma OAI.CubicTorus.corner_grid_518 line 1090
  139. lemma OAI.CubicTorus.corner_grid_519 line 1098
  140. lemma OAI.CubicTorus.corner_grid_520 line 1106
  141. lemma OAI.CubicTorus.corner_grid_521 line 1114
  142. lemma OAI.CubicTorus.corner_grid_522 line 1122
  143. theorem OAI.CubicTorus.corner_root_strict line 1130