OAI/Computability/PerfectCompleteness/Decoding/CutGroupedProjectionLemmas.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CutGroupedProjection.F2 line 16
  2. def OAI.PerfectCompleteness.CutGroupedProjection.cutProjection line 22
  3. def OAI.PerfectCompleteness.CutGroupedProjection.terminalPullback line 29
  4. def OAI.PerfectCompleteness.CutGroupedProjection.factorPullback line 37
  5. def OAI.PerfectCompleteness.CutGroupedProjection.tapePullback line 55
  6. theorem OAI.PerfectCompleteness.CutGroupedProjection.evaluate_tapePullback line 62
  7. theorem OAI.PerfectCompleteness.CutGroupedProjection.terminalFactor_pullback line 122
  8. theorem OAI.PerfectCompleteness.CutGroupedProjection.exteriorFactor_pullback line 148
  9. theorem OAI.PerfectCompleteness.CutGroupedProjection.splitTape_tapePullback line 184
  10. theorem OAI.PerfectCompleteness.CutGroupedProjection.evaluate_rebuild line 209
  11. abbrev OAI.PerfectCompleteness.OriginalScalarProjection.F2 line 252
  12. theorem OAI.PerfectCompleteness.OriginalScalarProjection.factor_eq line 258
  13. theorem OAI.PerfectCompleteness.OriginalScalarProjection.scalarExterior_eq line 280
  14. def OAI.PerfectCompleteness.OriginalScalarProjection.terminalPullback line 290
  15. def OAI.PerfectCompleteness.OriginalScalarProjection.factorPullback line 297
  16. def OAI.PerfectCompleteness.OriginalScalarProjection.tapePullback line 313
  17. theorem OAI.PerfectCompleteness.OriginalScalarProjection.evaluate_tapePullback line 320
  18. theorem OAI.PerfectCompleteness.OriginalScalarProjection.terminalFactor_pullback line 379
  19. theorem OAI.PerfectCompleteness.OriginalScalarProjection.exteriorFactor_pullback line 404
  20. theorem OAI.PerfectCompleteness.OriginalScalarProjection.prefixSplit_tapePullback line 440
  21. theorem OAI.PerfectCompleteness.OriginalScalarProjection.reconstruct_pullback_apply line 465
  22. theorem OAI.PerfectCompleteness.OriginalScalarProjection.reconstruct_pullback line 503