OAI/Computability/PerfectCompleteness/Foundations/WholeArrayPositiveSplit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.WholeArrayPositiveSplit.ScalarTape line 19
  2. instance OAI.PerfectCompleteness.WholeArrayPositiveSplit.scalarTapeFintype line 23
  3. def OAI.PerfectCompleteness.WholeArrayPositiveSplit.RestTape line 35
  4. def OAI.PerfectCompleteness.WholeArrayPositiveSplit.restTapeFintypeAux line 41
  5. instance OAI.PerfectCompleteness.WholeArrayPositiveSplit.restTapeFintype line 48
  6. abbrev OAI.PerfectCompleteness.WholeArrayPositiveSplit.Exterior line 53
  7. def OAI.PerfectCompleteness.WholeArrayPositiveSplit.scalarLaw line 57
  8. def OAI.PerfectCompleteness.WholeArrayPositiveSplit.restLaw line 62
  9. def OAI.PerfectCompleteness.WholeArrayPositiveSplit.exteriorLaw line 69
  10. def OAI.PerfectCompleteness.WholeArrayPositiveSplit.split line 75
  11. theorem OAI.PerfectCompleteness.WholeArrayPositiveSplit.split_law line 86
  12. theorem OAI.PerfectCompleteness.WholeArrayPositiveSplit.split_readout_law line 98
  13. def OAI.PerfectCompleteness.WholeArrayPositiveSplit.nodeArray line 114
  14. theorem OAI.PerfectCompleteness.WholeArrayPositiveSplit.nodeArray_split line 125