OAI/Computability/PerfectCompleteness/Decoding/LowerCutPairLemmas.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.LowerCutPair.F2 line 22
  2. abbrev OAI.PerfectCompleteness.LowerCutPair.Calls line 30
  3. abbrev OAI.PerfectCompleteness.LowerCutPair.Raw line 31
  4. abbrev OAI.PerfectCompleteness.LowerCutPair.NativeRows line 32
  5. abbrev OAI.PerfectCompleteness.LowerCutPair.NativeMatrix line 33
  6. def OAI.PerfectCompleteness.LowerCutPair.first line 35
  7. def OAI.PerfectCompleteness.LowerCutPair.fresh line 40
  8. def OAI.PerfectCompleteness.LowerCutPair.second line 43
  9. def OAI.PerfectCompleteness.LowerCutPair.arraysPair line 51
  10. theorem OAI.PerfectCompleteness.LowerCutPair.selected_second line 56
  11. theorem OAI.PerfectCompleteness.LowerCutPair.second_outside line 64
  12. theorem OAI.PerfectCompleteness.LowerCutPair.selected_quotient line 71
  13. def OAI.PerfectCompleteness.LowerCutPair.readRowsFresh line 82
  14. def OAI.PerfectCompleteness.LowerCutPair.selectPair line 87
  15. theorem OAI.PerfectCompleteness.LowerCutPair.selectPair_surjective line 92
  16. theorem OAI.PerfectCompleteness.LowerCutPair.readRowsFresh_eq line 97
  17. theorem OAI.PerfectCompleteness.LowerCutPair.readRowsFresh_law line 106
  18. def OAI.PerfectCompleteness.LowerCutPair.selectedPair line 120
  19. theorem OAI.PerfectCompleteness.LowerCutPair.selectedPair_law line 126
  20. def OAI.PerfectCompleteness.LowerCutPair.matrixPair line 142
  21. theorem OAI.PerfectCompleteness.LowerCutPair.matrixPair_law line 152
  22. def OAI.PerfectCompleteness.LowerCutDecoderForm.spaceEquiv line 190
  23. def OAI.PerfectCompleteness.LowerCutDecoderForm.form line 195
  24. theorem OAI.PerfectCompleteness.LowerCutDecoderForm.form_apply line 209
  25. theorem OAI.PerfectCompleteness.LowerCutDecoderForm.form_injective line 218
  26. def OAI.PerfectCompleteness.LowerCutDecoderForm.answer line 235
  27. def OAI.PerfectCompleteness.LowerCutDecoderForm.readForm line 240
  28. def OAI.PerfectCompleteness.LowerCutDecoderForm.first line 245
  29. def OAI.PerfectCompleteness.LowerCutDecoderForm.second line 251
  30. theorem OAI.PerfectCompleteness.LowerCutDecoderForm.fullCollision_readForm line 258
  31. theorem OAI.PerfectCompleteness.LowerCutDecoderForm.fullCollision_pair line 269