OAI/Computability/PerfectCompleteness/Sampling/SourceChildQuestionLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.SourceChildQuestionLaw.sourceLaw line 20
  2. def OAI.PerfectCompleteness.SourceChildQuestionLaw.assembleEquiv line 26
  3. theorem OAI.PerfectCompleteness.SourceChildQuestionLaw.assemble_child_law line 43
  4. theorem OAI.PerfectCompleteness.SourceChildQuestionLaw.uniform_product line 61
  5. theorem OAI.PerfectCompleteness.SourceChildQuestionLaw.uniform_equiv line 70
  6. theorem OAI.PerfectCompleteness.SourceChildQuestionLaw.sourceLaw_uniform line 79
  7. theorem OAI.PerfectCompleteness.SourceChildQuestionLaw.assemble_law line 85
  8. def OAI.PerfectCompleteness.SourceChildQuestionLaw.questions line 91
  9. def OAI.PerfectCompleteness.SourceChildQuestionLaw.splitPositions line 96
  10. theorem OAI.PerfectCompleteness.SourceChildQuestionLaw.questions_law line 105
  11. theorem OAI.PerfectCompleteness.SourceChildQuestionLaw.parentLeftSlots_eq line 122
  12. theorem OAI.PerfectCompleteness.SourceChildQuestionLaw.originalLaw_sources line 128
  13. theorem OAI.PerfectCompleteness.SourceChildQuestionLaw.originalLaw_questions line 136