OAI/Analysis/Triangular/Certificate/JetMatrix.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.columnTable line 9
  2. lemma OAI.AtomicTriangular.FiniteCertificate.columnTable_mem line 10
  3. def OAI.AtomicTriangular.FiniteCertificate.fullJetBox line 35
  4. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetBox_mem line 37
  5. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow0 line 44
  6. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow0_calc line 67
  7. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow0_mem line 70
  8. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow1 line 73
  9. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow1_calc line 96
  10. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow1_mem line 99
  11. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow2 line 102
  12. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow2_calc line 125
  13. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow2_mem line 128
  14. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow3 line 131
  15. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow3_calc line 154
  16. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow3_mem line 157
  17. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow4 line 160
  18. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow4_calc line 183
  19. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow4_mem line 186
  20. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow5 line 189
  21. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow5_calc line 212
  22. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow5_mem line 215
  23. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow6 line 218
  24. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow6_calc line 241
  25. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow6_mem line 244
  26. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow7 line 247
  27. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow7_calc line 270
  28. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow7_mem line 273
  29. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow8 line 276
  30. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow8_calc line 299
  31. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow8_mem line 302
  32. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow9 line 305
  33. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow9_calc line 328
  34. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow9_mem line 331
  35. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow10 line 334
  36. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow10_calc line 357
  37. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow10_mem line 360
  38. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow11 line 363
  39. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow11_calc line 386
  40. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow11_mem line 389
  41. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow12 line 392
  42. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow12_calc line 415
  43. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow12_mem line 418
  44. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow13 line 421
  45. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow13_calc line 444
  46. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow13_mem line 447
  47. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow14 line 450
  48. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow14_calc line 473
  49. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow14_mem line 476
  50. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow15 line 479
  51. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow15_calc line 502
  52. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow15_mem line 505
  53. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow16 line 508
  54. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow16_calc line 531
  55. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow16_mem line 534
  56. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow17 line 537
  57. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow17_calc line 560
  58. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow17_mem line 563
  59. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow18 line 566
  60. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow18_calc line 589
  61. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow18_mem line 592
  62. def OAI.AtomicTriangular.FiniteCertificate.fullJetRow19 line 595
  63. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow19_calc line 618
  64. lemma OAI.AtomicTriangular.FiniteCertificate.fullJetRow19_mem line 621
  65. def OAI.AtomicTriangular.FiniteCertificate.jetMatrixTable line 624
  66. lemma OAI.AtomicTriangular.FiniteCertificate.jetMatrixTable_mem line 625
  67. def OAI.AtomicTriangular.FiniteCertificate.RBox line 647
  68. lemma OAI.AtomicTriangular.FiniteCertificate.RBox_mem line 648
  69. def OAI.AtomicTriangular.FiniteCertificate.R0Box line 649
  70. lemma OAI.AtomicTriangular.FiniteCertificate.R0Box_mem line 650