OAI/Analysis/Triangular/Envelope/EnvelopePsiC.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC36 line 11
  2. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC36_calc line 12
  3. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC36_pre line 15
  4. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC36_mem line 18
  5. def OAI.AtomicTriangular.FiniteCertificate.psiC36 line 24
  6. lemma OAI.AtomicTriangular.FiniteCertificate.psiC36_calc line 25
  7. lemma OAI.AtomicTriangular.FiniteCertificate.psiC36_mem line 28
  8. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC37 line 41
  9. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC37_calc line 42
  10. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC37_pre line 45
  11. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC37_mem line 48
  12. def OAI.AtomicTriangular.FiniteCertificate.psiC37 line 54
  13. lemma OAI.AtomicTriangular.FiniteCertificate.psiC37_calc line 55
  14. lemma OAI.AtomicTriangular.FiniteCertificate.psiC37_mem line 58
  15. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC39 line 71
  16. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC39_calc line 72
  17. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC39_pre line 75
  18. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC39_mem line 78
  19. def OAI.AtomicTriangular.FiniteCertificate.psiC39 line 84
  20. lemma OAI.AtomicTriangular.FiniteCertificate.psiC39_calc line 85
  21. lemma OAI.AtomicTriangular.FiniteCertificate.psiC39_mem line 88
  22. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC40 line 101
  23. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC40_calc line 102
  24. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC40_pre line 105
  25. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC40_mem line 108
  26. def OAI.AtomicTriangular.FiniteCertificate.psiC40 line 114
  27. lemma OAI.AtomicTriangular.FiniteCertificate.psiC40_calc line 115
  28. lemma OAI.AtomicTriangular.FiniteCertificate.psiC40_mem line 118
  29. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC43 line 131
  30. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC43_calc line 132
  31. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC43_pre line 135
  32. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC43_mem line 138
  33. def OAI.AtomicTriangular.FiniteCertificate.psiC43 line 144
  34. lemma OAI.AtomicTriangular.FiniteCertificate.psiC43_calc line 145
  35. lemma OAI.AtomicTriangular.FiniteCertificate.psiC43_mem line 148
  36. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC45 line 161
  37. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC45_calc line 162
  38. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC45_pre line 165
  39. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC45_mem line 168
  40. def OAI.AtomicTriangular.FiniteCertificate.psiC45 line 174
  41. lemma OAI.AtomicTriangular.FiniteCertificate.psiC45_calc line 175
  42. lemma OAI.AtomicTriangular.FiniteCertificate.psiC45_mem line 178
  43. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC48 line 191
  44. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC48_calc line 192
  45. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC48_pre line 195
  46. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC48_mem line 198
  47. def OAI.AtomicTriangular.FiniteCertificate.psiC48 line 204
  48. lemma OAI.AtomicTriangular.FiniteCertificate.psiC48_calc line 205
  49. lemma OAI.AtomicTriangular.FiniteCertificate.psiC48_mem line 208
  50. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC49 line 221
  51. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC49_calc line 222
  52. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC49_pre line 225
  53. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC49_mem line 228
  54. def OAI.AtomicTriangular.FiniteCertificate.psiC49 line 234
  55. lemma OAI.AtomicTriangular.FiniteCertificate.psiC49_calc line 235
  56. lemma OAI.AtomicTriangular.FiniteCertificate.psiC49_mem line 238
  57. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC52 line 251
  58. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC52_calc line 252
  59. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC52_pre line 255
  60. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC52_mem line 258
  61. def OAI.AtomicTriangular.FiniteCertificate.psiC52 line 264
  62. lemma OAI.AtomicTriangular.FiniteCertificate.psiC52_calc line 265
  63. lemma OAI.AtomicTriangular.FiniteCertificate.psiC52_mem line 268
  64. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC55 line 281
  65. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC55_calc line 282
  66. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC55_pre line 285
  67. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC55_mem line 288
  68. def OAI.AtomicTriangular.FiniteCertificate.psiC55 line 294
  69. lemma OAI.AtomicTriangular.FiniteCertificate.psiC55_calc line 295
  70. lemma OAI.AtomicTriangular.FiniteCertificate.psiC55_mem line 298
  71. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC57 line 311
  72. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC57_calc line 312
  73. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC57_pre line 315
  74. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC57_mem line 318
  75. def OAI.AtomicTriangular.FiniteCertificate.psiC57 line 324
  76. lemma OAI.AtomicTriangular.FiniteCertificate.psiC57_calc line 325
  77. lemma OAI.AtomicTriangular.FiniteCertificate.psiC57_mem line 328
  78. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC25 line 341
  79. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC25_calc line 342
  80. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC25_pre line 345
  81. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC25_mem line 348
  82. def OAI.AtomicTriangular.FiniteCertificate.psiC25 line 354
  83. lemma OAI.AtomicTriangular.FiniteCertificate.psiC25_calc line 355
  84. lemma OAI.AtomicTriangular.FiniteCertificate.psiC25_mem line 358
  85. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC27 line 367
  86. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC27_calc line 368
  87. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC27_pre line 371
  88. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC27_mem line 374
  89. def OAI.AtomicTriangular.FiniteCertificate.psiC27 line 380
  90. lemma OAI.AtomicTriangular.FiniteCertificate.psiC27_calc line 381
  91. lemma OAI.AtomicTriangular.FiniteCertificate.psiC27_mem line 384
  92. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC28 line 393
  93. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC28_calc line 394
  94. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC28_pre line 397
  95. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC28_mem line 400
  96. def OAI.AtomicTriangular.FiniteCertificate.psiC28 line 406
  97. lemma OAI.AtomicTriangular.FiniteCertificate.psiC28_calc line 407
  98. lemma OAI.AtomicTriangular.FiniteCertificate.psiC28_mem line 410
  99. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpC31 line 419
  100. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC31_calc line 420
  101. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC31_pre line 423
  102. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpC31_mem line 426
  103. def OAI.AtomicTriangular.FiniteCertificate.psiC31 line 432
  104. lemma OAI.AtomicTriangular.FiniteCertificate.psiC31_calc line 433
  105. lemma OAI.AtomicTriangular.FiniteCertificate.psiC31_mem line 436