OAI/Computability/PerfectCompleteness/Decoding/WholeCutGroupedProjection.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.WholeCutGroupedProjection.F2 line 15
  2. def OAI.PerfectCompleteness.WholeCutGroupedProjection.evaluateGrouped line 21
  3. theorem OAI.PerfectCompleteness.WholeCutGroupedProjection.evaluateGrouped_root line 29
  4. theorem OAI.PerfectCompleteness.WholeCutGroupedProjection.evaluateGrouped_selected line 41
  5. theorem OAI.PerfectCompleteness.WholeCutGroupedProjection.evaluateGrouped_ordinary line 54
  6. theorem OAI.PerfectCompleteness.WholeCutGroupedProjection.cast_exterior_parts line 67
  7. theorem OAI.PerfectCompleteness.WholeCutGroupedProjection.exterior_equiv_step line 78
  8. theorem OAI.PerfectCompleteness.WholeCutGroupedProjection.assembleArrays_pullback line 95
  9. theorem OAI.PerfectCompleteness.WholeCutGroupedProjection.bucket_evaluate_pullback line 104
  10. theorem OAI.PerfectCompleteness.WholeCutGroupedProjection.evaluateGrouped_pullback line 122
  11. theorem OAI.PerfectCompleteness.WholeCutGroupedProjection.exteriorAt_pullback line 218
  12. theorem OAI.PerfectCompleteness.WholeCutGroupedProjection.fillChildren_pullback line 236
  13. theorem OAI.PerfectCompleteness.WholeCutGroupedProjection.physicalTape_pullback line 261
  14. theorem OAI.PerfectCompleteness.WholeCutGroupedProjection.fullJoint_physicalTape_pullback line 293