OAI/Analysis/Triangular/Signs/ExceptionalSign1.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.ex1r0 line 9
  2. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r0_calc line 17
  3. def OAI.AtomicTriangular.FiniteCertificate.ex1r1 line 20
  4. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r1_calc line 28
  5. def OAI.AtomicTriangular.FiniteCertificate.ex1r2 line 31
  6. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r2_calc line 39
  7. def OAI.AtomicTriangular.FiniteCertificate.ex1r3 line 42
  8. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r3_calc line 50
  9. def OAI.AtomicTriangular.FiniteCertificate.ex1r4 line 53
  10. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r4_calc line 61
  11. def OAI.AtomicTriangular.FiniteCertificate.ex1r5 line 64
  12. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r5_calc line 72
  13. def OAI.AtomicTriangular.FiniteCertificate.ex1r6 line 75
  14. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r6_calc line 83
  15. def OAI.AtomicTriangular.FiniteCertificate.ex1r7 line 86
  16. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r7_calc line 94
  17. def OAI.AtomicTriangular.FiniteCertificate.ex1r8 line 97
  18. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r8_calc line 105
  19. def OAI.AtomicTriangular.FiniteCertificate.ex1r9 line 108
  20. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r9_calc line 116
  21. def OAI.AtomicTriangular.FiniteCertificate.ex1r10 line 119
  22. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r10_calc line 127
  23. def OAI.AtomicTriangular.FiniteCertificate.ex1r11 line 130
  24. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r11_calc line 138
  25. def OAI.AtomicTriangular.FiniteCertificate.ex1r12 line 141
  26. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r12_calc line 149
  27. def OAI.AtomicTriangular.FiniteCertificate.ex1r13 line 152
  28. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r13_calc line 160
  29. def OAI.AtomicTriangular.FiniteCertificate.ex1r14 line 163
  30. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r14_calc line 171
  31. def OAI.AtomicTriangular.FiniteCertificate.ex1r15 line 174
  32. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r15_calc line 182
  33. def OAI.AtomicTriangular.FiniteCertificate.ex1r16 line 185
  34. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r16_calc line 193
  35. def OAI.AtomicTriangular.FiniteCertificate.ex1r17 line 196
  36. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r17_calc line 204
  37. def OAI.AtomicTriangular.FiniteCertificate.ex1r18 line 207
  38. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r18_calc line 215
  39. def OAI.AtomicTriangular.FiniteCertificate.ex1r19 line 218
  40. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r19_calc line 226
  41. def OAI.AtomicTriangular.FiniteCertificate.ex1r20 line 229
  42. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r20_calc line 237
  43. def OAI.AtomicTriangular.FiniteCertificate.ex1r21 line 240
  44. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r21_calc line 248
  45. def OAI.AtomicTriangular.FiniteCertificate.ex1r22 line 251
  46. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r22_calc line 259
  47. def OAI.AtomicTriangular.FiniteCertificate.ex1r line 262
  48. lemma OAI.AtomicTriangular.FiniteCertificate.ex1r_mem line 263
  49. def OAI.AtomicTriangular.FiniteCertificate.ex1b0 line 291
  50. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b0_calc line 299
  51. def OAI.AtomicTriangular.FiniteCertificate.ex1b1 line 302
  52. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b1_calc line 310
  53. def OAI.AtomicTriangular.FiniteCertificate.ex1b2 line 313
  54. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b2_calc line 321
  55. def OAI.AtomicTriangular.FiniteCertificate.ex1b3 line 324
  56. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b3_calc line 332
  57. def OAI.AtomicTriangular.FiniteCertificate.ex1b4 line 335
  58. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b4_calc line 343
  59. def OAI.AtomicTriangular.FiniteCertificate.ex1b5 line 346
  60. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b5_calc line 354
  61. def OAI.AtomicTriangular.FiniteCertificate.ex1b6 line 357
  62. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b6_calc line 365
  63. def OAI.AtomicTriangular.FiniteCertificate.ex1b7 line 368
  64. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b7_calc line 376
  65. def OAI.AtomicTriangular.FiniteCertificate.ex1b8 line 379
  66. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b8_calc line 387
  67. def OAI.AtomicTriangular.FiniteCertificate.ex1b9 line 390
  68. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b9_calc line 398
  69. def OAI.AtomicTriangular.FiniteCertificate.ex1b10 line 401
  70. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b10_calc line 409
  71. def OAI.AtomicTriangular.FiniteCertificate.ex1b11 line 412
  72. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b11_calc line 420
  73. def OAI.AtomicTriangular.FiniteCertificate.ex1b12 line 423
  74. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b12_calc line 431
  75. def OAI.AtomicTriangular.FiniteCertificate.ex1b13 line 434
  76. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b13_calc line 442
  77. def OAI.AtomicTriangular.FiniteCertificate.ex1b14 line 445
  78. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b14_calc line 453
  79. def OAI.AtomicTriangular.FiniteCertificate.ex1b15 line 456
  80. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b15_calc line 464
  81. def OAI.AtomicTriangular.FiniteCertificate.ex1b16 line 467
  82. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b16_calc line 475
  83. def OAI.AtomicTriangular.FiniteCertificate.ex1b17 line 478
  84. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b17_calc line 486
  85. def OAI.AtomicTriangular.FiniteCertificate.ex1b18 line 489
  86. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b18_calc line 497
  87. def OAI.AtomicTriangular.FiniteCertificate.ex1b19 line 500
  88. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b19_calc line 508
  89. def OAI.AtomicTriangular.FiniteCertificate.ex1b20 line 511
  90. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b20_calc line 519
  91. def OAI.AtomicTriangular.FiniteCertificate.ex1b21 line 522
  92. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b21_calc line 530
  93. def OAI.AtomicTriangular.FiniteCertificate.ex1b22 line 533
  94. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b22_calc line 541
  95. def OAI.AtomicTriangular.FiniteCertificate.ex1b line 544
  96. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b_mem line 545
  97. lemma OAI.AtomicTriangular.FiniteCertificate.ex1b_lower line 573
  98. lemma OAI.AtomicTriangular.FiniteCertificate.exceptional_sign_1 line 578