OAI/Computability/PerfectCompleteness/Construction/AscendingBranchingLemmas.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.AscendingBranching.exists_prior_sequence line 15
  2. def OAI.PerfectCompleteness.AscendingBranching.CubeErrors line 28
  3. theorem OAI.PerfectCompleteness.AscendingBranching.exists_ascending_cubes line 35
  4. theorem OAI.PerfectCompleteness.AscendingBranching.exists_common_accuracy line 52
  5. structure OAI.PerfectCompleteness.DescendingRows.Exclusion line 85
  6. theorem OAI.PerfectCompleteness.DescendingRows.exclusion_exists line 103
  7. def OAI.PerfectCompleteness.DescendingRows.lowerChoice line 111
  8. theorem OAI.PerfectCompleteness.DescendingRows.exists_rows line 116
  9. def OAI.PerfectCompleteness.DescendingRows.commonCutoff line 135
  10. theorem OAI.PerfectCompleteness.DescendingRows.commonCutoff_pos line 138
  11. theorem OAI.PerfectCompleteness.DescendingRows.cutoff_le_common line 141
  12. theorem OAI.PerfectCompleteness.DescendingRows.error_at_common line 151
  13. def OAI.PerfectCompleteness.DescendingRows.treeRows line 160
  14. theorem OAI.PerfectCompleteness.DescendingRows.tree_pair_requirement line 163
  15. theorem OAI.PerfectCompleteness.DescendingRows.tree_cutoff_le_common line 171