OAI/Computability/PerfectCompleteness/Construction/SourceQuestionKernelJoint.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.SourceQuestionKernelJoint.kernelJoint_pushforward_first line 16
  2. abbrev OAI.PerfectCompleteness.SourceQuestionKernelJoint.ChoiceTuple line 29
  3. def OAI.PerfectCompleteness.SourceQuestionKernelJoint.sourceEquiv line 32
  4. def OAI.PerfectCompleteness.SourceQuestionKernelJoint.sources line 39
  5. theorem OAI.PerfectCompleteness.SourceQuestionKernelJoint.sources_eq_join line 45
  6. theorem OAI.PerfectCompleteness.SourceQuestionKernelJoint.sourceLaw_sourceEquiv line 52
  7. def OAI.PerfectCompleteness.SourceQuestionKernelJoint.groupEquiv line 77
  8. theorem OAI.PerfectCompleteness.SourceQuestionKernelJoint.groupEquiv_raw line 85
  9. theorem OAI.PerfectCompleteness.SourceQuestionKernelJoint.originalLaw_group line 90