OAI/Computability/PerfectCompleteness/Foundations/ProjectedCallRestriction.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ProjectedCallRestriction.rawRestrict line 18
  2. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.rawRestrict_calls line 27
  3. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.rawRestrict_arrays line 33
  4. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.rawRestrict_surjective line 39
  5. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.uniform_restrict_law line 50
  6. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.rawRestrict_pullback line 59
  7. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.lifted_restrict_law line 67
  8. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.mixture_restrict_law line 83
  9. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.sparse_pushforward line 98
  10. def OAI.PerfectCompleteness.ProjectedCallRestriction.restrictChildren line 115
  11. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.sparse_restrict_law line 122
  12. def OAI.PerfectCompleteness.ProjectedCallRestriction.assembledRestrict line 151
  13. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.assembledRestrict_calls line 160
  14. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.assembledRestrict_arrays line 167
  15. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.assemble_restrict line 173
  16. theorem OAI.PerfectCompleteness.ProjectedCallRestriction.assembled_restrict_law line 181