OAI/Computability/PerfectCompleteness/Foundations/ProjectedCutChoices.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.ProjectedCutChoices.mixture_const line 17
  2. theorem OAI.PerfectCompleteness.ProjectedCutChoices.product_mixture line 25
  3. theorem OAI.PerfectCompleteness.ProjectedCutChoices.lifted_keep line 34
  4. def OAI.PerfectCompleteness.ProjectedCutChoices.childDomain line 62
  5. def OAI.PerfectCompleteness.ProjectedCutChoices.childProjection line 66
  6. abbrev OAI.PerfectCompleteness.ProjectedCutChoices.Choices line 74
  7. def OAI.PerfectCompleteness.ProjectedCutChoices.selectedSlots line 76
  8. def OAI.PerfectCompleteness.ProjectedCutChoices.selectedProjection line 81
  9. def OAI.PerfectCompleteness.ProjectedCutChoices.choicesLaw line 86
  10. def OAI.PerfectCompleteness.ProjectedCutChoices.childLaw line 91
  11. theorem OAI.PerfectCompleteness.ProjectedCutChoices.row_eq_mixture line 96
  12. theorem OAI.PerfectCompleteness.ProjectedCutChoices.raw_eq_mixture line 118
  13. theorem OAI.PerfectCompleteness.ProjectedCutChoices.fixed_assembly line 135
  14. theorem OAI.PerfectCompleteness.ProjectedCutChoices.assembled_eq_mixture line 157