OAI/Computability/PerfectCompleteness/Construction/OriginalOwnBucketSplit.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.valuesChildrenFintype line 21
  2. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.OtherIndex line 28
  3. instance OAI.PerfectCompleteness.OriginalOwnBucketSplit.otherIndexFintype line 34
  4. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.sumEmpty line 44
  5. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.swapFirstSum line 53
  6. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.indexEquiv line 65
  7. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.indexEquiv_ownBucket line 75
  8. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.indexEquiv_symm_inl line 88
  9. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.otherCall line 95
  10. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.indexEquiv_otherCall line 99
  11. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.otherCall_injective line 104
  12. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.otherCall_ne_ownBucket line 110
  13. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.valuesEquiv line 118
  14. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.valuesEquiv_own line 124
  15. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.valuesEquiv_other line 132
  16. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.valuesEquiv_symm_own line 138
  17. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.valuesEquiv_symm_other line 147
  18. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.valuesEquiv_law line 156
  19. abbrev OAI.PerfectCompleteness.OriginalOwnBucketSplit.BucketTape line 173
  20. abbrev OAI.PerfectCompleteness.OriginalOwnBucketSplit.OtherValues line 177
  21. abbrev OAI.PerfectCompleteness.OriginalOwnBucketSplit.Complement line 181
  22. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.recordEquiv line 185
  23. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.assembleRecord line 211
  24. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.recordEquiv_own line 217
  25. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.split_assembleRecord line 224
  26. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.assembleRecord_split line 231
  27. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.assembleRecord_exterior line 238
  28. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.assembleRecord_below line 243
  29. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.assembleRecord_own line 248
  30. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.assembleRecord_other line 256
  31. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.assembleRecord_nonown_eq line 264
  32. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.complementLaw line 285
  33. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.independent_record_split line 294
  34. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.actualComplementLaw line 320
  35. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.recordLaw_split line 329
  36. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.uniform_record_split line 342
  37. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.uniform_record_split_bucketLaw line 351
  38. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.uniform_assembleRecord line 361
  39. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.zeroOwnReconstruction line 374
  40. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.reconstruct_assembleRecord_outside line 379
  41. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.background line 395
  42. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.background_assembleRecord line 402
  43. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.background_record line 411
  44. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.backgroundLaw line 427
  45. def OAI.PerfectCompleteness.OriginalOwnBucketSplit.actualBackgroundLaw line 434
  46. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.recordLaw_own_background line 442
  47. theorem OAI.PerfectCompleteness.OriginalOwnBucketSplit.uniform_own_background line 475