OAI/Computability/PerfectCompleteness/Sampling/RestrictionRowsLaw.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.RestrictionRowsLaw.rowsLinear line 23
  2. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.rowsLinear_apply line 37
  3. def OAI.PerfectCompleteness.RestrictionRowsLaw.fromRows line 40
  4. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.rowsLinear_fromRows line 43
  5. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.rowsLinear_surjective line 50
  6. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.rowsLinear_injective line 54
  7. def OAI.PerfectCompleteness.RestrictionRowsLaw.rowsEquiv line 62
  8. def OAI.PerfectCompleteness.RestrictionRowsLaw.selectLinear line 70
  9. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.selectLinear_surjective line 75
  10. def OAI.PerfectCompleteness.RestrictionRowsLaw.selectedRowsLinear line 79
  11. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.selectedRowsLinear_apply line 83
  12. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.selectedRowsLinear_surjective line 86
  13. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.uniform_rowsLinear line 96
  14. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.uniform_rows_law line 102
  15. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.uniform_add_left line 110
  16. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.uniform_translated_rows line 119
  17. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.uniform_selectedRowsLinear line 130
  18. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.uniform_selected_rows_law line 137
  19. def OAI.PerfectCompleteness.RestrictionRowsLaw.affineRow line 148
  20. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.coordinate_translate line 152
  21. def OAI.PerfectCompleteness.RestrictionRowsLaw.affineRowLaw line 169
  22. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.uniform_affine_rows_law line 172
  23. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.uniform_coordinate_translate_law line 181
  24. theorem OAI.PerfectCompleteness.RestrictionRowsLaw.uniform_selected_affine_rows_law line 197