OAI/Computability/PerfectCompleteness/Reduction/CompletionOutputLemmas.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.CompletionOutput.family line 24
  2. theorem OAI.PerfectCompleteness.CompletionOutput.family_size line 27
  3. theorem OAI.PerfectCompleteness.CompletionOutput.family_total_size line 34
  4. def OAI.PerfectCompleteness.CompletionOutput.construct line 44
  5. theorem OAI.PerfectCompleteness.CompletionOutput.construct_leftVertices line 47
  6. theorem OAI.PerfectCompleteness.CompletionOutput.construct_rightVertices line 50
  7. theorem OAI.PerfectCompleteness.CompletionOutput.construct_edge_count line 53
  8. theorem OAI.PerfectCompleteness.CompletionOutput.construct_word_count line 61
  9. theorem OAI.PerfectCompleteness.CompletionOutput.construct_value_le line 71
  10. theorem OAI.PerfectCompleteness.CompletionOutput.construct_value_le_of_residual_bound line 79
  11. theorem OAI.PerfectCompleteness.CompletionOutput.construct_perfectlyComplete line 86
  12. theorem OAI.PerfectCompleteness.CompletionOutput.construct_soundAt line 93
  13. theorem OAI.PerfectCompleteness.CompletionParameters.residual_le_third line 116
  14. def OAI.PerfectCompleteness.CompletionParameters.embedFin line 127
  15. theorem OAI.PerfectCompleteness.CompletionParameters.construct_value_le_delta line 138
  16. theorem OAI.PerfectCompleteness.CompletionParameters.construct_soundAt_of_budget line 152
  17. theorem OAI.PerfectCompleteness.CompletionParameters.exists_target line 166