OAI/Computability/PerfectCompleteness/Decoding/ProjectedLowerFiber.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.ProjectedLowerFiber.lower line 24
  2. abbrev OAI.PerfectCompleteness.ProjectedLowerFiber.Scalar line 25
  3. abbrev OAI.PerfectCompleteness.ProjectedLowerFiber.Direction line 26
  4. def OAI.PerfectCompleteness.ProjectedLowerFiber.arraysAt line 28
  5. theorem OAI.PerfectCompleteness.ProjectedLowerFiber.rightInput_fixed line 34
  6. theorem OAI.PerfectCompleteness.ProjectedLowerFiber.rightLaw_fixed line 47
  7. def OAI.PerfectCompleteness.ProjectedLowerFiber.originalArraysAt line 65
  8. theorem OAI.PerfectCompleteness.ProjectedLowerFiber.originalArraysAt_eq_update line 71
  9. def OAI.PerfectCompleteness.ProjectedLowerFiber.inputAt line 89
  10. theorem OAI.PerfectCompleteness.ProjectedLowerFiber.inputAt_eq_lowerInput line 96
  11. abbrev OAI.PerfectCompleteness.ProjectedLowerFiber.UpperTable line 112
  12. def OAI.PerfectCompleteness.ProjectedLowerFiber.upperAt line 116
  13. theorem OAI.PerfectCompleteness.ProjectedLowerFiber.upperTarget_eq_dualMap line 123