OAI/Computability/PerfectCompleteness/Decoding/DecoderSourcePullback.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.DecoderSourcePullback.F2 line 15
  2. def OAI.PerfectCompleteness.DecoderSourcePullback.relativeCut line 20
  3. def OAI.PerfectCompleteness.DecoderSourcePullback.selectedCut line 36
  4. theorem OAI.PerfectCompleteness.DecoderSourcePullback.upperBranch line 41
  5. theorem OAI.PerfectCompleteness.DecoderSourcePullback.restriction_projection line 48
  6. theorem OAI.PerfectCompleteness.DecoderSourcePullback.squareEmbedding_pullback line 58
  7. theorem OAI.PerfectCompleteness.DecoderSourcePullback.squarePullback_product line 74
  8. def OAI.PerfectCompleteness.DecoderSourcePullback.upperTarget line 80
  9. theorem OAI.PerfectCompleteness.DecoderSourcePullback.upperTarget_apply line 85
  10. theorem OAI.PerfectCompleteness.DecoderSourcePullback.embed_squareEmbedding line 95
  11. theorem OAI.PerfectCompleteness.DecoderSourcePullback.functional_upperTarget line 114
  12. theorem OAI.PerfectCompleteness.DecoderSourcePullback.form_upperTarget line 143
  13. theorem OAI.PerfectCompleteness.DecoderSourcePullback.form_eq_of_target_error line 168