OAI/Analysis/Triangular/Certificate/ParamU.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.UplusCachedBox line 9
  2. lemma OAI.AtomicTriangular.FiniteCertificate.UplusCachedBox_mem line 10
  3. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow0 line 11
  4. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow0_calc line 12
  5. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow1 line 15
  6. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow1_calc line 16
  7. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow2 line 19
  8. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow2_calc line 20
  9. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow3 line 23
  10. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow3_calc line 24
  11. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow4 line 27
  12. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow4_calc line 28
  13. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow5 line 31
  14. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow5_calc line 32
  15. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow6 line 35
  16. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow6_calc line 36
  17. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow7 line 39
  18. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow7_calc line 40
  19. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow8 line 43
  20. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow8_calc line 44
  21. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow9 line 47
  22. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow9_calc line 48
  23. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow10 line 51
  24. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow10_calc line 52
  25. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow11 line 55
  26. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow11_calc line 56
  27. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow12 line 59
  28. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow12_calc line 60
  29. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow13 line 63
  30. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow13_calc line 64
  31. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow14 line 67
  32. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow14_calc line 68
  33. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow15 line 71
  34. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow15_calc line 72
  35. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow16 line 75
  36. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow16_calc line 76
  37. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow17 line 79
  38. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow17_calc line 80
  39. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow18 line 83
  40. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow18_calc line 84
  41. def OAI.AtomicTriangular.FiniteCertificate.UplusTableRow19 line 87
  42. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTableRow19_calc line 88
  43. def OAI.AtomicTriangular.FiniteCertificate.UplusTable line 91
  44. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTable_calc line 92
  45. lemma OAI.AtomicTriangular.FiniteCertificate.UplusTable_mem line 114
  46. def OAI.AtomicTriangular.FiniteCertificate.UminusCachedBox line 117
  47. lemma OAI.AtomicTriangular.FiniteCertificate.UminusCachedBox_mem line 118
  48. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow0 line 119
  49. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow0_calc line 120
  50. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow1 line 123
  51. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow1_calc line 124
  52. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow2 line 127
  53. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow2_calc line 128
  54. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow3 line 131
  55. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow3_calc line 132
  56. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow4 line 135
  57. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow4_calc line 136
  58. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow5 line 139
  59. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow5_calc line 140
  60. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow6 line 143
  61. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow6_calc line 144
  62. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow7 line 147
  63. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow7_calc line 148
  64. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow8 line 151
  65. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow8_calc line 152
  66. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow9 line 155
  67. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow9_calc line 156
  68. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow10 line 159
  69. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow10_calc line 160
  70. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow11 line 163
  71. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow11_calc line 164
  72. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow12 line 167
  73. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow12_calc line 168
  74. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow13 line 171
  75. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow13_calc line 172
  76. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow14 line 175
  77. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow14_calc line 176
  78. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow15 line 179
  79. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow15_calc line 180
  80. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow16 line 183
  81. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow16_calc line 184
  82. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow17 line 187
  83. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow17_calc line 188
  84. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow18 line 191
  85. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow18_calc line 192
  86. def OAI.AtomicTriangular.FiniteCertificate.UminusTableRow19 line 195
  87. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTableRow19_calc line 196
  88. def OAI.AtomicTriangular.FiniteCertificate.UminusTable line 199
  89. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTable_calc line 200
  90. lemma OAI.AtomicTriangular.FiniteCertificate.UminusTable_mem line 222