OAI/Computability/PerfectCompleteness/Decoding/CanonicalUpperDirectionSplit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.Complement line 18
  2. def OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.splitEquiv line 22
  3. def OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.complement line 27
  4. def OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.assemble line 31
  5. theorem OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.split_selected line 36
  6. theorem OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.complement_apply line 40
  7. theorem OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.assemble_at_upper line 44
  8. theorem OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.assemble_at_other line 49
  9. theorem OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.assemble_split line 57
  10. theorem OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.lower_preserved line 62
  11. def OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.complementLaw line 69
  12. theorem OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.split_law line 73
  13. theorem OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.assemble_law line 78
  14. theorem OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.selected_law line 93
  15. theorem OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.probability_split line 98
  16. theorem OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.probability_complement_first line 106
  17. theorem OAI.PerfectCompleteness.CanonicalUpperDirectionSplit.lower_choice_preserved line 116