OAI/Computability/PerfectCompleteness/Construction/SourceQuestionCutSplit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceQuestionCutSplit.OutsideLeaf line 18
  2. abbrev OAI.PerfectCompleteness.SourceQuestionCutSplit.OutsideQuestions line 21
  3. def OAI.PerfectCompleteness.SourceQuestionCutSplit.restrict line 24
  4. def OAI.PerfectCompleteness.SourceQuestionCutSplit.outside line 29
  5. def OAI.PerfectCompleteness.SourceQuestionCutSplit.join line 33
  6. theorem OAI.PerfectCompleteness.SourceQuestionCutSplit.join_at_cut line 39
  7. theorem OAI.PerfectCompleteness.SourceQuestionCutSplit.join_outside line 48
  8. theorem OAI.PerfectCompleteness.SourceQuestionCutSplit.join_restrict line 54
  9. def OAI.PerfectCompleteness.SourceQuestionCutSplit.splitEquiv line 62
  10. theorem OAI.PerfectCompleteness.SourceQuestionCutSplit.splitEquiv_apply line 75
  11. theorem OAI.PerfectCompleteness.SourceQuestionCutSplit.splitEquiv_symm_apply line 79
  12. theorem OAI.PerfectCompleteness.SourceQuestionCutSplit.split_law line 83
  13. theorem OAI.PerfectCompleteness.SourceQuestionCutSplit.join_eq_fill line 97
  14. theorem OAI.PerfectCompleteness.SourceQuestionCutSplit.sourceSlots_restrict line 111
  15. theorem OAI.PerfectCompleteness.SourceQuestionCutSplit.sourceSlots_fill line 117
  16. theorem OAI.PerfectCompleteness.SourceQuestionCutSplit.sourceSlots_join line 139