OAI/Computability/PerfectCompleteness/Foundations/ProjectedWholeCut.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.ProjectedWholeCut.product_mixture line 18
  2. theorem OAI.PerfectCompleteness.ProjectedWholeCut.lifted_assembled_congr line 35
  3. def OAI.PerfectCompleteness.ProjectedWholeCut.fullSlots line 60
  4. theorem OAI.PerfectCompleteness.ProjectedWholeCut.fill_native line 65
  5. def OAI.PerfectCompleteness.ProjectedWholeCut.fullProjection line 68
  6. theorem OAI.PerfectCompleteness.ProjectedWholeCut.cut_fullSlots line 77
  7. theorem OAI.PerfectCompleteness.ProjectedWholeCut.cut_fullProjection line 85
  8. theorem OAI.PerfectCompleteness.ProjectedWholeCut.fullSlots_outside line 100
  9. theorem OAI.PerfectCompleteness.ProjectedWholeCut.fullProjection_outside line 110
  10. theorem OAI.PerfectCompleteness.ProjectedWholeCut.fixed_law line 125
  11. def OAI.PerfectCompleteness.ProjectedWholeCut.arrayLaw line 149
  12. theorem OAI.PerfectCompleteness.ProjectedWholeCut.reconstruct_assembled_law line 156
  13. theorem OAI.PerfectCompleteness.ProjectedWholeCut.old_arrayLaw_eq line 171