OAI/Geometry/Convex/GeneralMahler/Middle/Verified.lean

GitHub source file

128 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK0_11 line 6
2. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK11_22 line 10
3. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK0_22 line 14
4. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK22_33 line 15
5. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK33_45 line 19
6. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK22_45 line 23
7. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK0_45 line 24
8. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK45_56 line 25
9. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK56_67 line 29
10. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK45_67 line 33
11. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK67_78 line 34
12. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK78_90 line 38
13. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK67_90 line 42
14. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK45_90 line 43
15. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK0_90 line 44
16. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK90_101 line 45
17. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK101_112 line 49
18. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK90_112 line 53
19. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK112_123 line 54
20. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK123_135 line 58
21. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK112_135 line 62
22. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK90_135 line 63
23. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK135_146 line 64
24. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK146_157 line 68
25. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK135_157 line 72
26. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK157_168 line 73
27. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK168_180 line 77
28. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK157_180 line 81
29. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK135_180 line 82
30. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK90_180 line 83
31. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK0_180 line 84
32. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK180_191 line 85
33. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK191_202 line 89
34. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK180_202 line 93
35. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK202_213 line 94
36. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK213_225 line 98
37. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK202_225 line 102
38. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK180_225 line 103
39. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK225_236 line 104
40. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK236_247 line 108
41. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK225_247 line 112
42. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK247_258 line 113
43. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK258_270 line 117
44. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK247_270 line 121
45. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK225_270 line 122
46. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK180_270 line 123
47. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK270_281 line 124
48. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK281_292 line 128
49. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK270_292 line 132
50. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK292_303 line 133
51. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK303_315 line 137
52. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK292_315 line 141
53. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK270_315 line 142
54. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK315_326 line 143
55. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK326_337 line 147
56. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK315_337 line 151
57. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK337_348 line 152
58. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK348_360 line 156
59. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK337_360 line 160
60. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK315_360 line 161
61. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK270_360 line 162
62. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK180_360 line 163
63. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK0_360 line 164
64. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK360_371 line 165
65. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK371_382 line 169
66. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK360_382 line 173
67. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK382_393 line 174
68. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK393_405 line 178
69. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK382_405 line 182
70. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK360_405 line 183
71. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK405_416 line 184
72. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK416_427 line 188
73. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK405_427 line 192
74. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK427_438 line 193
75. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK438_450 line 197
76. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK427_450 line 201
77. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK405_450 line 202
78. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK360_450 line 203
79. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK450_461 line 204
80. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK461_472 line 208
81. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK450_472 line 212
82. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK472_483 line 213
83. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK483_495 line 217
84. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK472_495 line 221
85. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK450_495 line 222
86. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK495_506 line 223
87. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK506_517 line 227
88. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK495_517 line 231
89. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK517_528 line 232
90. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK528_540 line 236
91. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK517_540 line 240
92. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK495_540 line 241
93. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK450_540 line 242
94. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK360_540 line 243
95. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK540_551 line 244
96. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK551_562 line 248
97. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK540_562 line 252
98. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK562_573 line 253
99. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK573_585 line 257
100. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK562_585 line 261
101. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK540_585 line 262
102. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK585_596 line 263
103. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK596_607 line 267
104. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK585_607 line 271
105. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK607_618 line 272
106. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK618_630 line 276
107. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK607_630 line 280
108. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK585_630 line 281
109. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK540_630 line 282
110. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK630_641 line 283
111. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK641_652 line 287
112. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK630_652 line 291
113. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK652_663 line 292
114. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK663_675 line 296
115. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK652_675 line 300
116. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK630_675 line 301
117. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK675_686 line 302
118. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK686_697 line 306
119. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK675_697 line 310
120. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK697_708 line 311
121. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK708_720 line 315
122. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK697_720 line 319
123. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK675_720 line 320
124. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK630_720 line 321
125. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK540_720 line 322
126. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK360_720 line 323
127. lemma OAI.GeneralMahler.SCal.Mid.Tab.CK0_720 line 324
128. lemma OAI.GeneralMahler.SCal.Mid.Tab.checkedP line 325