OAI/Computability/PerfectCompleteness/Decoding/ChildAssemblyProjection.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ChildAssemblyProjection.childProjection line 19
  2. theorem OAI.PerfectCompleteness.ChildAssemblyProjection.restrictChild_projection line 25
  3. theorem OAI.PerfectCompleteness.ChildAssemblyProjection.recursiveSum_pullback line 31
  4. def OAI.PerfectCompleteness.ChildAssemblyProjection.childPullback line 49
  5. theorem OAI.PerfectCompleteness.ChildAssemblyProjection.childPullback_fin line 69
  6. def OAI.PerfectCompleteness.ChildAssemblyProjection.rawPullback line 75
  7. def OAI.PerfectCompleteness.ChildAssemblyProjection.assembledPullback line 87
  8. theorem OAI.PerfectCompleteness.ChildAssemblyProjection.assemble_pullback line 107
  9. theorem OAI.PerfectCompleteness.ChildAssemblyProjection.assemble_comp_pullback line 118
  10. def OAI.PerfectCompleteness.ChildAssemblyProjection.evaluate line 126
  11. theorem OAI.PerfectCompleteness.ChildAssemblyProjection.evaluate_pullback line 133
  12. theorem OAI.PerfectCompleteness.ChildAssemblyProjection.evaluate_assemble_pullback line 139
  13. theorem OAI.PerfectCompleteness.ChildAssemblyProjection.pushforward_assemble line 147
  14. theorem OAI.PerfectCompleteness.ChildAssemblyProjection.uniform_projected_assembly line 158