OAI/Analysis/Triangular/Envelope/EnvelopePsiD.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD36 line 11
  2. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD36_calc line 12
  3. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD36_pre line 15
  4. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD36_mem line 18
  5. def OAI.AtomicTriangular.FiniteCertificate.psiD36 line 24
  6. lemma OAI.AtomicTriangular.FiniteCertificate.psiD36_calc line 25
  7. lemma OAI.AtomicTriangular.FiniteCertificate.psiD36_mem line 28
  8. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD37 line 41
  9. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD37_calc line 42
  10. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD37_pre line 45
  11. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD37_mem line 48
  12. def OAI.AtomicTriangular.FiniteCertificate.psiD37 line 54
  13. lemma OAI.AtomicTriangular.FiniteCertificate.psiD37_calc line 55
  14. lemma OAI.AtomicTriangular.FiniteCertificate.psiD37_mem line 58
  15. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD39 line 71
  16. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD39_calc line 72
  17. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD39_pre line 75
  18. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD39_mem line 78
  19. def OAI.AtomicTriangular.FiniteCertificate.psiD39 line 84
  20. lemma OAI.AtomicTriangular.FiniteCertificate.psiD39_calc line 85
  21. lemma OAI.AtomicTriangular.FiniteCertificate.psiD39_mem line 88
  22. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD40 line 101
  23. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD40_calc line 102
  24. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD40_pre line 105
  25. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD40_mem line 108
  26. def OAI.AtomicTriangular.FiniteCertificate.psiD40 line 114
  27. lemma OAI.AtomicTriangular.FiniteCertificate.psiD40_calc line 115
  28. lemma OAI.AtomicTriangular.FiniteCertificate.psiD40_mem line 118
  29. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD43 line 131
  30. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD43_calc line 132
  31. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD43_pre line 135
  32. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD43_mem line 138
  33. def OAI.AtomicTriangular.FiniteCertificate.psiD43 line 144
  34. lemma OAI.AtomicTriangular.FiniteCertificate.psiD43_calc line 145
  35. lemma OAI.AtomicTriangular.FiniteCertificate.psiD43_mem line 148
  36. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD45 line 161
  37. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD45_calc line 162
  38. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD45_pre line 165
  39. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD45_mem line 168
  40. def OAI.AtomicTriangular.FiniteCertificate.psiD45 line 174
  41. lemma OAI.AtomicTriangular.FiniteCertificate.psiD45_calc line 175
  42. lemma OAI.AtomicTriangular.FiniteCertificate.psiD45_mem line 178
  43. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD48 line 191
  44. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD48_calc line 192
  45. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD48_pre line 195
  46. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD48_mem line 198
  47. def OAI.AtomicTriangular.FiniteCertificate.psiD48 line 204
  48. lemma OAI.AtomicTriangular.FiniteCertificate.psiD48_calc line 205
  49. lemma OAI.AtomicTriangular.FiniteCertificate.psiD48_mem line 208
  50. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD49 line 221
  51. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD49_calc line 222
  52. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD49_pre line 225
  53. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD49_mem line 228
  54. def OAI.AtomicTriangular.FiniteCertificate.psiD49 line 234
  55. lemma OAI.AtomicTriangular.FiniteCertificate.psiD49_calc line 235
  56. lemma OAI.AtomicTriangular.FiniteCertificate.psiD49_mem line 238
  57. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD52 line 251
  58. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD52_calc line 252
  59. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD52_pre line 255
  60. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD52_mem line 258
  61. def OAI.AtomicTriangular.FiniteCertificate.psiD52 line 264
  62. lemma OAI.AtomicTriangular.FiniteCertificate.psiD52_calc line 265
  63. lemma OAI.AtomicTriangular.FiniteCertificate.psiD52_mem line 268
  64. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD55 line 281
  65. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD55_calc line 282
  66. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD55_pre line 285
  67. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD55_mem line 288
  68. def OAI.AtomicTriangular.FiniteCertificate.psiD55 line 294
  69. lemma OAI.AtomicTriangular.FiniteCertificate.psiD55_calc line 295
  70. lemma OAI.AtomicTriangular.FiniteCertificate.psiD55_mem line 298
  71. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD57 line 311
  72. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD57_calc line 312
  73. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD57_pre line 315
  74. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD57_mem line 318
  75. def OAI.AtomicTriangular.FiniteCertificate.psiD57 line 324
  76. lemma OAI.AtomicTriangular.FiniteCertificate.psiD57_calc line 325
  77. lemma OAI.AtomicTriangular.FiniteCertificate.psiD57_mem line 328
  78. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD25 line 341
  79. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD25_calc line 342
  80. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD25_pre line 345
  81. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD25_mem line 348
  82. def OAI.AtomicTriangular.FiniteCertificate.psiD25 line 354
  83. lemma OAI.AtomicTriangular.FiniteCertificate.psiD25_calc line 355
  84. lemma OAI.AtomicTriangular.FiniteCertificate.psiD25_mem line 358
  85. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD27 line 367
  86. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD27_calc line 368
  87. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD27_pre line 371
  88. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD27_mem line 374
  89. def OAI.AtomicTriangular.FiniteCertificate.psiD27 line 380
  90. lemma OAI.AtomicTriangular.FiniteCertificate.psiD27_calc line 381
  91. lemma OAI.AtomicTriangular.FiniteCertificate.psiD27_mem line 384
  92. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD28 line 393
  93. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD28_calc line 394
  94. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD28_pre line 397
  95. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD28_mem line 400
  96. def OAI.AtomicTriangular.FiniteCertificate.psiD28 line 406
  97. lemma OAI.AtomicTriangular.FiniteCertificate.psiD28_calc line 407
  98. lemma OAI.AtomicTriangular.FiniteCertificate.psiD28_mem line 410
  99. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpD31 line 419
  100. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD31_calc line 420
  101. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD31_pre line 423
  102. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpD31_mem line 426
  103. def OAI.AtomicTriangular.FiniteCertificate.psiD31 line 432
  104. lemma OAI.AtomicTriangular.FiniteCertificate.psiD31_calc line 433
  105. lemma OAI.AtomicTriangular.FiniteCertificate.psiD31_mem line 436