OAI/Computability/PerfectCompleteness/Sampling/OriginalWholeCutLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.OriginalWholeCutLaw.product_map_record line 17
  2. def OAI.PerfectCompleteness.OriginalWholeCutLaw.valuesBelowFintype line 33
  3. theorem OAI.PerfectCompleteness.OriginalWholeCutLaw.childrenAt_law line 43
  4. def OAI.PerfectCompleteness.OriginalWholeCutLaw.belowArraysLaw line 65
  5. theorem OAI.PerfectCompleteness.OriginalWholeCutLaw.below_product_law line 71
  6. theorem OAI.PerfectCompleteness.OriginalWholeCutLaw.belowEvaluate_law line 108
  7. def OAI.PerfectCompleteness.OriginalWholeCutLaw.valuesLaw line 115
  8. theorem OAI.PerfectCompleteness.OriginalWholeCutLaw.callsEvaluate_law line 123
  9. theorem OAI.PerfectCompleteness.OriginalWholeCutLaw.numberedValues_law line 137
  10. def OAI.PerfectCompleteness.OriginalWholeCutLaw.recordLaw line 163
  11. theorem OAI.PerfectCompleteness.OriginalWholeCutLaw.readRecord_law line 171
  12. theorem OAI.PerfectCompleteness.OriginalWholeCutLaw.reconstruct_law line 215