OAI/Computability/PerfectCompleteness/Decoding/LowerCutPairBackground.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.LowerCutPairBackground.F2 line 17
  2. abbrev OAI.PerfectCompleteness.LowerCutPairBackground.Complement line 25
  3. abbrev OAI.PerfectCompleteness.LowerCutPairBackground.NativeRows line 26
  4. abbrev OAI.PerfectCompleteness.LowerCutPairBackground.NativeMatrix line 27
  5. abbrev OAI.PerfectCompleteness.LowerCutPairBackground.Observation line 29
  6. def OAI.PerfectCompleteness.LowerCutPairBackground.splitObservation line 32
  7. theorem OAI.PerfectCompleteness.LowerCutPairBackground.splitObservation_surjective line 42
  8. def OAI.PerfectCompleteness.LowerCutPairBackground.observe line 52
  9. theorem OAI.PerfectCompleteness.LowerCutPairBackground.observe_law line 56
  10. theorem OAI.PerfectCompleteness.LowerCutPairBackground.observe_rows line 72
  11. theorem OAI.PerfectCompleteness.LowerCutPairBackground.observe_fresh line 79
  12. def OAI.PerfectCompleteness.LowerCutPairBackground.rowPair line 82
  13. theorem OAI.PerfectCompleteness.LowerCutPairBackground.rowPair_law line 89
  14. def OAI.PerfectCompleteness.LowerCutPairBackground.matrixPair line 120
  15. theorem OAI.PerfectCompleteness.LowerCutPairBackground.matrixPair_law line 127
  16. def OAI.PerfectCompleteness.LowerCutPairBackground.backgroundArrays line 152
  17. def OAI.PerfectCompleteness.LowerCutPairBackground.installRows line 157
  18. theorem OAI.PerfectCompleteness.LowerCutPairBackground.reconstruct_merge line 162
  19. theorem OAI.PerfectCompleteness.LowerCutPairBackground.first_eq_installRows line 176
  20. theorem OAI.PerfectCompleteness.LowerCutPairBackground.replace_replace line 195
  21. theorem OAI.PerfectCompleteness.LowerCutPairBackground.second_eq_installRows line 207
  22. def OAI.PerfectCompleteness.LowerCutPairBackground.installMatrix line 224
  23. theorem OAI.PerfectCompleteness.LowerCutPairBackground.arraysPair_eq line 228
  24. theorem OAI.PerfectCompleteness.LowerCutPairBackground.arraysPair_law line 241
  25. theorem OAI.PerfectCompleteness.LowerCutPairBackground.installMatrix_eq_update line 260
  26. theorem OAI.PerfectCompleteness.LowerCutPairBackground.installMatrix_outside line 269
  27. theorem OAI.PerfectCompleteness.LowerCutPairBackground.backgroundOf_installMatrix line 276
  28. theorem OAI.PerfectCompleteness.LowerCutPairBackground.upperMatrix_installMatrix line 285