OAI/Computability/PerfectCompleteness/Decoding/OriginalWholeCutProjection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.OriginalWholeCutProjection.exterior_eq line 20
  2. def OAI.PerfectCompleteness.OriginalWholeCutProjection.exteriorEquiv line 45
  3. theorem OAI.PerfectCompleteness.OriginalWholeCutProjection.exteriorEquiv_law line 51
  4. theorem OAI.PerfectCompleteness.OriginalWholeCutProjection.cast_exterior_parts line 61
  5. theorem OAI.PerfectCompleteness.OriginalWholeCutProjection.exteriorEquiv_step line 72
  6. theorem OAI.PerfectCompleteness.OriginalWholeCutProjection.reconstruct_root line 88
  7. theorem OAI.PerfectCompleteness.OriginalWholeCutProjection.reconstruct_selected line 98
  8. theorem OAI.PerfectCompleteness.OriginalWholeCutProjection.reconstruct_ordinary line 111
  9. theorem OAI.PerfectCompleteness.OriginalWholeCutProjection.bucket_evaluate_pullback line 124
  10. theorem OAI.PerfectCompleteness.OriginalWholeCutProjection.reconstruct_pullback line 142
  11. theorem OAI.PerfectCompleteness.OriginalWholeCutProjection.reconstruct_numbered_pullback line 241
  12. theorem OAI.PerfectCompleteness.OriginalWholeCutProjection.fixed_projected_law line 256