OAI/Computability/PerfectCompleteness/Decoding/LowerDirectionFiber.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.LowerDirectionFiber.exists_pivot line 22
  2. def OAI.PerfectCompleteness.LowerDirectionFiber.pivot line 30
  3. theorem OAI.PerfectCompleteness.LowerDirectionFiber.pivot_value line 32
  4. abbrev OAI.PerfectCompleteness.LowerDirectionFiber.Other line 35
  5. abbrev OAI.PerfectCompleteness.LowerDirectionFiber.Rows line 36
  6. abbrev OAI.PerfectCompleteness.LowerDirectionFiber.Complement line 37
  7. theorem OAI.PerfectCompleteness.LowerDirectionFiber.scalar_count line 39
  8. def OAI.PerfectCompleteness.LowerDirectionFiber.complement line 48
  9. def OAI.PerfectCompleteness.LowerDirectionFiber.restore line 51
  10. theorem OAI.PerfectCompleteness.LowerDirectionFiber.restore_pivot line 54
  11. theorem OAI.PerfectCompleteness.LowerDirectionFiber.restore_other line 57
  12. theorem OAI.PerfectCompleteness.LowerDirectionFiber.complement_restore line 61
  13. theorem OAI.PerfectCompleteness.LowerDirectionFiber.restore_complement line 66
  14. def OAI.PerfectCompleteness.LowerDirectionFiber.split line 74
  15. theorem OAI.PerfectCompleteness.LowerDirectionFiber.split_apply line 80
  16. def OAI.PerfectCompleteness.LowerDirectionFiber.replace line 83
  17. theorem OAI.PerfectCompleteness.LowerDirectionFiber.complement_replace line 86
  18. theorem OAI.PerfectCompleteness.LowerDirectionFiber.replace_eq line 90
  19. def OAI.PerfectCompleteness.LowerDirectionFiber.fiberEquiv line 102
  20. instance OAI.PerfectCompleteness.LowerDirectionFiber.fiberNonempty line 113
  21. theorem OAI.PerfectCompleteness.LowerDirectionFiber.quotient_replace line 116
  22. theorem OAI.PerfectCompleteness.LowerDirectionFiber.scalar_complement_eq line 131
  23. def OAI.PerfectCompleteness.LowerDirectionFiber.quotientQuery line 154
  24. theorem OAI.PerfectCompleteness.LowerDirectionFiber.quotientQuery_replace line 157
  25. theorem OAI.PerfectCompleteness.LowerDirectionFiber.quotientQuery_eq_iff line 162
  26. theorem OAI.PerfectCompleteness.LowerDirectionFiber.response_replace line 178
  27. theorem OAI.PerfectCompleteness.LowerDirectionFiber.ofRows_add_rankOne line 184
  28. theorem OAI.PerfectCompleteness.LowerDirectionFiber.ofRows_replace line 193
  29. theorem OAI.PerfectCompleteness.LowerDirectionFiber.uniform_product line 206
  30. theorem OAI.PerfectCompleteness.LowerDirectionFiber.split_uniform line 216
  31. theorem OAI.PerfectCompleteness.LowerDirectionFiber.uniform_fiber line 222
  32. def OAI.PerfectCompleteness.LowerDirectionFiber.pairCoordinates line 234
  33. theorem OAI.PerfectCompleteness.LowerDirectionFiber.pairCoordinates_apply line 243
  34. def OAI.PerfectCompleteness.LowerDirectionFiber.fiberPairLaw line 246
  35. theorem OAI.PerfectCompleteness.LowerDirectionFiber.two_copy_law line 251
  36. theorem OAI.PerfectCompleteness.LowerDirectionFiber.resampled_pair_law line 267
  37. theorem OAI.PerfectCompleteness.LowerDirectionFiber.fiberPairLaw_eq_rankOne line 279
  38. theorem OAI.PerfectCompleteness.LowerDirectionFiber.matrix_pair_law line 294