OAI/Computability/PerfectCompleteness/Foundations/WholeArraySubtreeSplit.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.WholeArraySubtreeSplit.subtreeSlots line 20
  2. def OAI.PerfectCompleteness.WholeArraySubtreeSplit.Complement line 25
  3. def OAI.PerfectCompleteness.WholeArraySubtreeSplit.complementFintypeAux line 34
  4. instance OAI.PerfectCompleteness.WholeArraySubtreeSplit.complementFintype line 46
  5. theorem OAI.PerfectCompleteness.WholeArraySubtreeSplit.complementNonemptyAux line 52
  6. instance OAI.PerfectCompleteness.WholeArraySubtreeSplit.complementNonempty line 64
  7. def OAI.PerfectCompleteness.WholeArraySubtreeSplit.splitEquiv line 70
  8. def OAI.PerfectCompleteness.WholeArraySubtreeSplit.extract line 106
  9. theorem OAI.PerfectCompleteness.WholeArraySubtreeSplit.extract_refl line 112
  10. theorem OAI.PerfectCompleteness.WholeArraySubtreeSplit.extract_step line 117
  11. def OAI.PerfectCompleteness.WholeArraySubtreeSplit.restrictArrays line 124
  12. theorem OAI.PerfectCompleteness.WholeArraySubtreeSplit.restrictArrays_evaluate line 132
  13. def OAI.PerfectCompleteness.WholeArraySubtreeSplit.complementLaw line 147
  14. theorem OAI.PerfectCompleteness.WholeArraySubtreeSplit.uniform_product line 159
  15. theorem OAI.PerfectCompleteness.WholeArraySubtreeSplit.uniform_pushforward_equiv line 168
  16. theorem OAI.PerfectCompleteness.WholeArraySubtreeSplit.rootTapeLaw_eq_uniform line 177
  17. theorem OAI.PerfectCompleteness.WholeArraySubtreeSplit.tapeLaw_eq_uniform line 192
  18. theorem OAI.PerfectCompleteness.WholeArraySubtreeSplit.complementLaw_eq_uniform line 221
  19. theorem OAI.PerfectCompleteness.WholeArraySubtreeSplit.splitEquiv_tapeLaw line 245
  20. theorem OAI.PerfectCompleteness.WholeArraySubtreeSplit.extract_tapeLaw line 255
  21. theorem OAI.PerfectCompleteness.WholeArraySubtreeSplit.restrictArrays_law line 265