OAI/Analysis/Triangular/Signs/ExceptionalSign3.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.ex3r0 line 9
  2. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r0_calc line 17
  3. def OAI.AtomicTriangular.FiniteCertificate.ex3r1 line 20
  4. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r1_calc line 28
  5. def OAI.AtomicTriangular.FiniteCertificate.ex3r2 line 31
  6. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r2_calc line 39
  7. def OAI.AtomicTriangular.FiniteCertificate.ex3r3 line 42
  8. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r3_calc line 50
  9. def OAI.AtomicTriangular.FiniteCertificate.ex3r4 line 53
  10. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r4_calc line 61
  11. def OAI.AtomicTriangular.FiniteCertificate.ex3r5 line 64
  12. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r5_calc line 72
  13. def OAI.AtomicTriangular.FiniteCertificate.ex3r6 line 75
  14. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r6_calc line 83
  15. def OAI.AtomicTriangular.FiniteCertificate.ex3r7 line 86
  16. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r7_calc line 94
  17. def OAI.AtomicTriangular.FiniteCertificate.ex3r8 line 97
  18. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r8_calc line 105
  19. def OAI.AtomicTriangular.FiniteCertificate.ex3r9 line 108
  20. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r9_calc line 116
  21. def OAI.AtomicTriangular.FiniteCertificate.ex3r10 line 119
  22. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r10_calc line 127
  23. def OAI.AtomicTriangular.FiniteCertificate.ex3r11 line 130
  24. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r11_calc line 138
  25. def OAI.AtomicTriangular.FiniteCertificate.ex3r12 line 141
  26. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r12_calc line 149
  27. def OAI.AtomicTriangular.FiniteCertificate.ex3r13 line 152
  28. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r13_calc line 160
  29. def OAI.AtomicTriangular.FiniteCertificate.ex3r14 line 163
  30. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r14_calc line 171
  31. def OAI.AtomicTriangular.FiniteCertificate.ex3r15 line 174
  32. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r15_calc line 182
  33. def OAI.AtomicTriangular.FiniteCertificate.ex3r16 line 185
  34. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r16_calc line 193
  35. def OAI.AtomicTriangular.FiniteCertificate.ex3r17 line 196
  36. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r17_calc line 204
  37. def OAI.AtomicTriangular.FiniteCertificate.ex3r18 line 207
  38. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r18_calc line 215
  39. def OAI.AtomicTriangular.FiniteCertificate.ex3r19 line 218
  40. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r19_calc line 226
  41. def OAI.AtomicTriangular.FiniteCertificate.ex3r20 line 229
  42. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r20_calc line 237
  43. def OAI.AtomicTriangular.FiniteCertificate.ex3r21 line 240
  44. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r21_calc line 248
  45. def OAI.AtomicTriangular.FiniteCertificate.ex3r22 line 251
  46. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r22_calc line 259
  47. def OAI.AtomicTriangular.FiniteCertificate.ex3r line 262
  48. lemma OAI.AtomicTriangular.FiniteCertificate.ex3r_mem line 263
  49. def OAI.AtomicTriangular.FiniteCertificate.ex3b0 line 291
  50. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b0_calc line 299
  51. def OAI.AtomicTriangular.FiniteCertificate.ex3b1 line 302
  52. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b1_calc line 310
  53. def OAI.AtomicTriangular.FiniteCertificate.ex3b2 line 313
  54. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b2_calc line 321
  55. def OAI.AtomicTriangular.FiniteCertificate.ex3b3 line 324
  56. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b3_calc line 332
  57. def OAI.AtomicTriangular.FiniteCertificate.ex3b4 line 335
  58. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b4_calc line 343
  59. def OAI.AtomicTriangular.FiniteCertificate.ex3b5 line 346
  60. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b5_calc line 354
  61. def OAI.AtomicTriangular.FiniteCertificate.ex3b6 line 357
  62. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b6_calc line 365
  63. def OAI.AtomicTriangular.FiniteCertificate.ex3b7 line 368
  64. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b7_calc line 376
  65. def OAI.AtomicTriangular.FiniteCertificate.ex3b8 line 379
  66. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b8_calc line 387
  67. def OAI.AtomicTriangular.FiniteCertificate.ex3b9 line 390
  68. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b9_calc line 398
  69. def OAI.AtomicTriangular.FiniteCertificate.ex3b10 line 401
  70. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b10_calc line 409
  71. def OAI.AtomicTriangular.FiniteCertificate.ex3b11 line 412
  72. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b11_calc line 420
  73. def OAI.AtomicTriangular.FiniteCertificate.ex3b12 line 423
  74. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b12_calc line 431
  75. def OAI.AtomicTriangular.FiniteCertificate.ex3b13 line 434
  76. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b13_calc line 442
  77. def OAI.AtomicTriangular.FiniteCertificate.ex3b14 line 445
  78. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b14_calc line 453
  79. def OAI.AtomicTriangular.FiniteCertificate.ex3b15 line 456
  80. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b15_calc line 464
  81. def OAI.AtomicTriangular.FiniteCertificate.ex3b16 line 467
  82. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b16_calc line 475
  83. def OAI.AtomicTriangular.FiniteCertificate.ex3b17 line 478
  84. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b17_calc line 486
  85. def OAI.AtomicTriangular.FiniteCertificate.ex3b18 line 489
  86. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b18_calc line 497
  87. def OAI.AtomicTriangular.FiniteCertificate.ex3b19 line 500
  88. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b19_calc line 508
  89. def OAI.AtomicTriangular.FiniteCertificate.ex3b20 line 511
  90. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b20_calc line 519
  91. def OAI.AtomicTriangular.FiniteCertificate.ex3b21 line 522
  92. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b21_calc line 530
  93. def OAI.AtomicTriangular.FiniteCertificate.ex3b22 line 533
  94. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b22_calc line 541
  95. def OAI.AtomicTriangular.FiniteCertificate.ex3b line 544
  96. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b_mem line 545
  97. lemma OAI.AtomicTriangular.FiniteCertificate.ex3b_lower line 573
  98. lemma OAI.AtomicTriangular.FiniteCertificate.exceptional_sign_3 line 578