OAI/Computability/PerfectCompleteness/Algebra/MatrixTriangularFoldingLemmas.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.MatrixTriangularFolding.query_add line 22
  2. theorem OAI.PerfectCompleteness.MatrixTriangularFolding.response_add line 34
  3. theorem OAI.PerfectCompleteness.MatrixTriangularFolding.response_add_side line 44
  4. theorem OAI.PerfectCompleteness.MatrixTriangularFolding.response_add_selected line 51
  5. def OAI.PerfectCompleteness.MatrixTriangularFolding.sideFunctional line 59
  6. theorem OAI.PerfectCompleteness.MatrixTriangularFolding.sideFunctional_at_image line 63
  7. def OAI.PerfectCompleteness.MatrixTriangularFolding.liftCorrection line 71
  8. def OAI.PerfectCompleteness.MatrixTriangularFolding.correction line 75
  9. theorem OAI.PerfectCompleteness.MatrixTriangularFolding.evaluate_liftCorrection line 80
  10. theorem OAI.PerfectCompleteness.MatrixTriangularFolding.response_add_correction line 89
  11. theorem OAI.PerfectCompleteness.MatrixTriangularFolding.correction_rankOne line 98
  12. def OAI.PerfectCompleteness.RepresentativeMatrixTable.Determined line 122
  13. theorem OAI.PerfectCompleteness.RepresentativeMatrixTable.determined_comap line 125
  14. def OAI.PerfectCompleteness.RepresentativeMatrixTable.sideEvaluation line 131
  15. theorem OAI.PerfectCompleteness.RepresentativeMatrixTable.sideEvaluation_at_image line 136
  16. def OAI.PerfectCompleteness.RepresentativeMatrixTable.correctionFunctional line 145
  17. def OAI.PerfectCompleteness.RepresentativeMatrixTable.representative line 148
  18. def OAI.PerfectCompleteness.RepresentativeMatrixTable.response line 152
  19. def OAI.PerfectCompleteness.RepresentativeMatrixTable.partialTable line 155
  20. theorem OAI.PerfectCompleteness.RepresentativeMatrixTable.raw_response line 161
  21. def OAI.PerfectCompleteness.RepresentativeMatrixTable.normalizeOutput line 184
  22. theorem OAI.PerfectCompleteness.RepresentativeMatrixTable.response_eq_normalize line 187
  23. def OAI.PerfectCompleteness.RepresentativeMatrixTable.normalizeQuotient line 200
  24. theorem OAI.PerfectCompleteness.RepresentativeMatrixTable.project_normalize_shift line 205
  25. theorem OAI.PerfectCompleteness.RepresentativeMatrixTable.accepted_response_in_fiber line 221
  26. theorem OAI.PerfectCompleteness.RepresentativeMatrixTable.card_accepted_responses_le_two line 233