OAI/Computability/PerfectCompleteness/Construction/LocalReconstruction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.LocalReconstruction.Retained line 16
  2. def OAI.PerfectCompleteness.LocalReconstruction.retain line 20
  3. abbrev OAI.PerfectCompleteness.LocalReconstruction.Summands line 24
  4. def OAI.PerfectCompleteness.LocalReconstruction.retainedCut line 29
  5. def OAI.PerfectCompleteness.LocalReconstruction.cutCall line 34
  6. theorem OAI.PerfectCompleteness.LocalReconstruction.cutCall_factors line 42
  7. theorem OAI.PerfectCompleteness.LocalReconstruction.cutCall_ignores_clean line 50
  8. theorem OAI.PerfectCompleteness.LocalReconstruction.actual_sum_eq_cutCall line 57
  9. theorem OAI.PerfectCompleteness.LocalReconstruction.actual_sum_ignores_clean line 75
  10. inductive OAI.PerfectCompleteness.LocalReconstruction.Recipe line 83
  11. def OAI.PerfectCompleteness.LocalReconstruction.Recipe.evaluate line 93
  12. theorem OAI.PerfectCompleteness.LocalReconstruction.Recipe.evaluate_factors line 99
  13. theorem OAI.PerfectCompleteness.LocalReconstruction.Recipe.evaluate_pullback line 108