OAI/Analysis/Triangular/Envelope/EnvelopePsiB.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpB1 line 10
  2. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB1_calc line 11
  3. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB1_pre line 14
  4. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB1_mem line 17
  5. def OAI.AtomicTriangular.FiniteCertificate.psiB1 line 23
  6. lemma OAI.AtomicTriangular.FiniteCertificate.psiB1_calc line 24
  7. lemma OAI.AtomicTriangular.FiniteCertificate.psiB1_mem line 27
  8. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpB3 line 36
  9. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB3_calc line 37
  10. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB3_pre line 40
  11. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB3_mem line 43
  12. def OAI.AtomicTriangular.FiniteCertificate.psiB3 line 49
  13. lemma OAI.AtomicTriangular.FiniteCertificate.psiB3_calc line 50
  14. lemma OAI.AtomicTriangular.FiniteCertificate.psiB3_mem line 53
  15. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpB4 line 62
  16. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB4_calc line 63
  17. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB4_pre line 66
  18. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB4_mem line 69
  19. def OAI.AtomicTriangular.FiniteCertificate.psiB4 line 75
  20. lemma OAI.AtomicTriangular.FiniteCertificate.psiB4_calc line 76
  21. lemma OAI.AtomicTriangular.FiniteCertificate.psiB4_mem line 79
  22. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpB7 line 88
  23. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB7_calc line 89
  24. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB7_pre line 92
  25. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB7_mem line 95
  26. def OAI.AtomicTriangular.FiniteCertificate.psiB7 line 101
  27. lemma OAI.AtomicTriangular.FiniteCertificate.psiB7_calc line 102
  28. lemma OAI.AtomicTriangular.FiniteCertificate.psiB7_mem line 105
  29. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpB9 line 114
  30. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB9_calc line 115
  31. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB9_pre line 118
  32. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB9_mem line 121
  33. def OAI.AtomicTriangular.FiniteCertificate.psiB9 line 127
  34. lemma OAI.AtomicTriangular.FiniteCertificate.psiB9_calc line 128
  35. lemma OAI.AtomicTriangular.FiniteCertificate.psiB9_mem line 131
  36. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpB12 line 140
  37. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB12_calc line 141
  38. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB12_pre line 144
  39. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB12_mem line 147
  40. def OAI.AtomicTriangular.FiniteCertificate.psiB12 line 153
  41. lemma OAI.AtomicTriangular.FiniteCertificate.psiB12_calc line 154
  42. lemma OAI.AtomicTriangular.FiniteCertificate.psiB12_mem line 157
  43. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpB13 line 166
  44. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB13_calc line 167
  45. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB13_pre line 170
  46. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB13_mem line 173
  47. def OAI.AtomicTriangular.FiniteCertificate.psiB13 line 179
  48. lemma OAI.AtomicTriangular.FiniteCertificate.psiB13_calc line 180
  49. lemma OAI.AtomicTriangular.FiniteCertificate.psiB13_mem line 183
  50. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpB16 line 192
  51. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB16_calc line 193
  52. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB16_pre line 196
  53. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB16_mem line 199
  54. def OAI.AtomicTriangular.FiniteCertificate.psiB16 line 205
  55. lemma OAI.AtomicTriangular.FiniteCertificate.psiB16_calc line 206
  56. lemma OAI.AtomicTriangular.FiniteCertificate.psiB16_mem line 209
  57. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpB19 line 218
  58. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB19_calc line 219
  59. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB19_pre line 222
  60. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB19_mem line 225
  61. def OAI.AtomicTriangular.FiniteCertificate.psiB19 line 231
  62. lemma OAI.AtomicTriangular.FiniteCertificate.psiB19_calc line 232
  63. lemma OAI.AtomicTriangular.FiniteCertificate.psiB19_mem line 235
  64. def OAI.AtomicTriangular.FiniteCertificate.envelopeExpB21 line 244
  65. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB21_calc line 245
  66. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB21_pre line 248
  67. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeExpB21_mem line 251
  68. def OAI.AtomicTriangular.FiniteCertificate.psiB21 line 257
  69. lemma OAI.AtomicTriangular.FiniteCertificate.psiB21_calc line 258
  70. lemma OAI.AtomicTriangular.FiniteCertificate.psiB21_mem line 261