OAI/Computability/PerfectCompleteness/Decoding/UpperScalarFreshProjectionLemmas.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.UpperScalarFreshProjection.outside_append line 22
  2. theorem OAI.PerfectCompleteness.UpperScalarFreshProjection.restricted_outside_eq line 30
  3. theorem OAI.PerfectCompleteness.UpperScalarFreshProjection.restricted_keep line 36
  4. def OAI.PerfectCompleteness.UpperScalarFreshProjection.freshExteriorEquiv line 45
  5. theorem OAI.PerfectCompleteness.UpperScalarFreshProjection.freshExteriorEquiv_law line 54
  6. theorem OAI.PerfectCompleteness.UpperScalarFreshProjection.cutSpaceEquiv_HPullback line 65
  7. theorem OAI.PerfectCompleteness.UpperScalarFreshProjection.reconstructFresh_pullback line 81
  8. def OAI.PerfectCompleteness.UpperScalarPairComparison.pairLaw line 140
  9. theorem OAI.PerfectCompleteness.UpperScalarPairComparison.variation_le line 151
  10. theorem OAI.PerfectCompleteness.UpperScalarPairComparison.modified_original_variation line 168
  11. abbrev OAI.PerfectCompleteness.UpperStoppedBuckets.F2 line 211
  12. def OAI.PerfectCompleteness.UpperStoppedBuckets.stoppedRootBuckets line 217
  13. def OAI.PerfectCompleteness.UpperStoppedBuckets.stoppedBuckets line 227
  14. theorem OAI.PerfectCompleteness.UpperStoppedBuckets.extract_toStoppedTape line 235
  15. theorem OAI.PerfectCompleteness.UpperStoppedBuckets.rootBuckets_toStoppedTape line 252
  16. theorem OAI.PerfectCompleteness.UpperStoppedBuckets.upperBuckets_toStoppedTape line 263
  17. theorem OAI.PerfectCompleteness.UpperStoppedBuckets.reference_toStoppedTape line 276
  18. theorem OAI.PerfectCompleteness.UpperStoppedBuckets.joint_referenceLaw line 285